diff --git a/coq-builtin.elpi b/coq-builtin.elpi index 89b3ca746..2ad5fe7d1 100644 --- 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 index c1b4c76b6..d00b7eab3 100644 --- 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 ->