fix cbv doc

LPCIC · Jul 27, 2023 · f7db0f5 · f7db0f5
1 parent fe05972
commit f7db0f5
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 2 deletions.
diff --git a/coq-builtin.elpi b/coq-builtin.elpi
@@ -1462,7 +1462,8 @@ external pred coq.reduction.lazy.norm i:term, o:term.
 % beta and iota redexes
 external pred coq.reduction.lazy.bi-norm i:term, o:term.
 
-% [coq.reduction.cbv.norm T Tred] Puts T in weak head normal form.
+% [coq.reduction.cbv.norm T Tred] Puts T in normal form using the call by
+% value strategy.
 % Supported attributes:
 % - @redflags! (default coq.redflags.all)
 external pred coq.reduction.cbv.norm i:term, o:term.

diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
@@ -3386,7 +3386,7 @@ Supported attributes:
   MLCode(Pred("coq.reduction.cbv.norm",
     CIn(term,"T",
     COut(term,"Tred",
-    Read(proof_context, {|Puts T in weak head normal form.
+    Read(proof_context, {|Puts T in normal form using the call by value strategy.
 Supported attributes:
 - @redflags! (default coq.redflags.all)|}))),
     (fun t _ ~depth proof_context constraints state ->