Merge pull request #441 from Blaisorblade/red-docs

Clarify difference between coq.reduction.{vm,native}.norm
LPCIC · Mar 6, 2023 · c038e88 · c038e88
2 parents e4a354c + 80b8320
commit c038e88
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 7 deletions.
diff --git a/Makefile b/Makefile
@@ -99,6 +99,7 @@ Makefile.examples.coq Makefile.examples.coq.conf: _CoqProject.examples
 	@$(COQBIN)/coq_makefile -f _CoqProject.examples -o Makefile.examples.coq
 src/coq_elpi_builtins_HOAS.ml: elpi/coq-HOAS.elpi Makefile.coq.local
 	echo "(* Automatically generated from $<, don't edit *)" > $@
+	echo "(* Regenerate via 'make $@' *)" >> $@
 	echo "let code = {|" >> $@
 	cat $< >> $@
 	echo "|}" >> $@

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 =