Clarify difference between coq.reduction.{vm,native}.norm

LPCIC · Mar 5, 2023 · 9d523ab · 9d523ab
1 parent e4a354c
commit 9d523ab
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 7 deletions.
diff --git a/coq-builtin.elpi b/coq-builtin.elpi
@@ -1438,13 +1438,13 @@ external pred coq.reduction.lazy.bi-norm i:term, o:term.
 % - @redflags! (default coq.redflags.all)
 external pred coq.reduction.cbv.norm i:term, o:term.
 
-% [coq.reduction.vm.norm T Ty Tred] Puts T in normal form. Its type Ty can
-% be omitted (but is recomputed)
+% [coq.reduction.vm.norm T Ty Tred] Puts T in normal form using [vm_compute]'s
+% machinery. Its type Ty can be omitted (but is recomputed)
 external pred coq.reduction.vm.norm i:term, i:term, o:term.
 
-% [coq.reduction.native.norm T Ty Tred] Puts T in normal form. Its type Ty
-% can be omitted (but is recomputed). Falls back to vm.norm if native
-% compilation is not available.
+% [coq.reduction.native.norm T Ty Tred] Puts T in normal form using
+% [native_compute]'s machinery. Its type Ty can be omitted (but is recomputed).
+% Falls back to vm.norm if native compilation is not available.
 external pred coq.reduction.native.norm i:term, i:term, o:term.
 
 % [coq.reduction.native.available?] Is native compilation available on this

diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
@@ -3282,7 +3282,7 @@ Supported attributes:
     CIn(term,"T",
     CIn(B.unspecC term,"Ty",
     COut(term,"Tred",
-    Read(proof_context, "Puts T in normal form. Its type Ty can be omitted (but is recomputed)")))),
+    Read(proof_context, "Puts T in normal form using [vm_compute]'s machinery. Its type Ty can be omitted (but is recomputed)")))),
     (fun t ty _ ~depth proof_context constraints state ->
        let sigma = get_sigma state in
        let sigma, ty =
@@ -3297,7 +3297,7 @@ Supported attributes:
     CIn(term,"T",
     CIn(B.unspecC term,"Ty",
     COut(term,"Tred",
-    Read(proof_context, "Puts T in normal form. Its type Ty can be omitted (but is recomputed). Falls back to vm.norm if native compilation is not available.")))),
+    Read(proof_context, "Puts T in normal form using [native_compute]'s machinery. Its type Ty can be omitted (but is recomputed). Falls back to vm.norm if native compilation is not available.")))),
     (fun t ty _ ~depth proof_context constraints state ->
        let sigma = get_sigma state in
        let sigma, ty =