From 9d523ab7bf50be8d2cece3776dd7f12eb6b20a73 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Sun, 5 Mar 2023 00:22:41 +0100 Subject: [PATCH 1/2] Clarify difference between coq.reduction.{vm,native}.norm --- coq-builtin.elpi | 10 +++++----- src/coq_elpi_builtins.ml | 4 ++-- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/coq-builtin.elpi b/coq-builtin.elpi index 5fee40732..f37c2b181 100644 --- 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 index 7fdc4d4f2..be9ccd7b2 100644 --- 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 = From 80b8320cc971071b9ca58bb248faa602b339db37 Mon Sep 17 00:00:00 2001 From: "Paolo G. Giarrusso" Date: Mon, 6 Mar 2023 00:08:52 +0100 Subject: [PATCH 2/2] src/coq_elpi_builtins_HOAS.ml: document regeneration command inline --- Makefile | 1 + 1 file changed, 1 insertion(+) diff --git a/Makefile b/Makefile index 6e53c0438..bc9f91d6c 100644 --- 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 "|}" >> $@