Merge pull request #573 from LPCIC/fix-detype

fix detype

Author: gares

.nix/coq-nix-toolbox.nix

@@ -1 +1 @@
-"4e48948fa8252a2fc755182abdd4b199f4798724"
+"dd771a5001cd955514f2462cad7cdd90377530e3"

.nix/coq-overlays/coq-elpi/default.nix

@@ -10,7 +10,7 @@ with builtins; with lib; let
     { case = "8.16"; out = { version = "1.17.0"; };}
     { case = "8.17"; out = { version = "1.17.0"; };}
     { case = "8.18"; out = { version = "v1.18.1"; };}
-    { case = "8.19"; out = { version = "v1.18.1"; };}
+    { case = "8.19"; out = { version = "v1.18.2"; };}
   ] {} );
 in mkCoqDerivation {
   pname = "elpi";

.ocamlformat

@@ -0,0 +1 @@
+m=120

Changelog.md

@@ -1,5 +1,14 @@
 # Changelog
 
+## [2.0.2] - 22/01/2024
+
+Requires Elpi 1.18.1 and Coq 8.19.
+
+### API
+- Fix `coq.elaborate-*` does not erase the type annotation of `Let`s (regression
+  introduced in 2.0.1). This fix may introduce differences in generated names
+- Fix `coq.elaborate-*` are not affected anymore by printing options
+
 ## [2.0.1] - 29/12/2023
 
 Requires Elpi 1.18.1 and Coq 8.19.

Makefile

@@ -151,3 +151,6 @@ SPACE=$(XXX) $(YYY)
 apps/%.vo: force
 	@$(MAKE) -C apps/$(word 1,$(subst /, ,$*)) \
 		$(subst $(SPACE),/,$(wordlist 2,99,$(subst /, ,$*))).vo
+
+nix:
+	nix-shell --arg do-nothing true --run "updateNixToolBox & genNixActions"

apps/derive/tests/test_projK.v

@@ -59,11 +59,11 @@ Check eq_refl 0 : projEnvelope1 nat 1 1 (Envelope nat 0 1) = 0.
 Check projEnvelope2 : forall A, A -> A -> zeta A -> A.
 Check eq_refl 0 : projEnvelope2 nat 1 1 (Envelope nat 1 0) = 0.
 Check projRedex1 : forall A, A -> beta A -> A.
-Check projWhy1 : forall n : peano, match n with 
+Check projWhy1 : forall n : peano, match n return Type with 
                     | Zero => peano
                     | Succ _ => unit
                     end -> iota -> peano.
-Check projWhy2 : forall n : peano, match n with 
+Check projWhy2 : forall n : peano, match n return Type with 
                     | Zero => peano
                     | Succ _ => unit
                     end -> iota -> { i : peano & match i with Zero => peano | Succ _ => unit end }.

coq-elpi.opam

@@ -15,7 +15,7 @@ install: [ make "install" "COQBIN=%{bin}%/" "ELPIDIR=%{prefix}%/lib/elpi" ]
 depends: [
   "ocaml" {>= "4.09.0" }
   "stdlib-shims"
-  "elpi" {>= "1.18.1" & < "1.19.0~"}
+  "elpi" {>= "1.18.2" & < "1.19.0~"}
   "coq" {>= "8.19" & < "8.20~" }
   "dot-merlin-reader" {with-dev}
   "ocaml-lsp-server" {with-dev}

src/coq_elpi_builtins_synterp.ml

@@ -53,7 +53,7 @@ let scope = let open Conv in let open API.AlgebraicData in declare {
 
 let grafting = let open Conv in let open API.AlgebraicData in declare {
   ty = TyName "grafting";
-  doc = "Specify if the clause has to be grafted before or after a named clause";
+  doc = "Specify if the clause has to be grafted before, grafted after or replace a named clause";
   pp = (fun fmt _ -> Format.fprintf fmt "<todo>");
   constructors = [
     K("before","",A(id,N),
@@ -62,10 +62,13 @@ let grafting = let open Conv in let open API.AlgebraicData in declare {
     K("after","",A(id,N),
         B (fun x -> (`After,x)),
         M (fun ~ok ~ko -> function (`After,x) -> ok x | _ -> ko ()));
+    K("replace","",A(id,N),
+      B (fun x -> (`Replace,x)),
+      M (fun ~ok ~ko -> function (`Replace,x) -> ok x | _ -> ko ()));
   ]
 } |> CConv.(!<)
 
-type clause = string option * ([ `After | `Before ] * string) option * API.Data.term
+type clause = string option * ([ `After | `Before | `Replace ] * string) option * API.Data.term
 
 let clause = let open Conv in let open API.AlgebraicData in declare {
   ty = TyName "clause";

src/coq_elpi_builtins_synterp.mli

@@ -52,14 +52,14 @@ val set_accumulate_to_db_synterp :
 val prop : Data.term Conversion.t
 val id : string Conversion.t
 
-type clause = string option * ([ `After | `Before ] * string) option * Data.term
+type clause = string option * ([ `After | `Before | `Replace ] * string) option * Data.term
 
 val clause : clause Conversion.t
 
 type scope = ExecutionSite | CurrentModule | Library
 
 val scope : scope Conversion.t
-val grafting : ([ `After | `Before ] * string) Conversion.t
+val grafting : ([ `After | `Before | `Replace ] * string) Conversion.t
 val options : (Coq_elpi_HOAS.options, Data.constraints) ContextualConversion.ctx_readback
 val locate_module : BuiltIn.declaration
 val locate_module_type : BuiltIn.declaration