fixup merge

LPCIC · Oct 30, 2019 · ee8cd3c · ee8cd3c
1 parent 79b117a
commit ee8cd3c
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/coq-elpi.opam b/coq-elpi.opam
@@ -11,7 +11,7 @@ dev-repo: "git+https://github.com/LPCIC/coq-elpi"
 build: [ make "COQBIN=%{bin}%/" "ELPIDIR=%{prefix}%/lib/elpi" ]
 install: [ make "install" "COQBIN=%{bin}%/" "ELPIDIR=%{prefix}%/lib/elpi" ]
 depends: [
-  "elpi" {>= "1.7.0" & < "1.8.0~"}
+  "elpi" {>= "1.8.0" & < "1.9.0~"}
   "coq" {= "8.10.dev"}
   ]
 synopsis: "Elpi extension language for Coq"

diff --git a/theories/examples/example_reflexive_tactic.v b/theories/examples/example_reflexive_tactic.v
@@ -221,7 +221,7 @@ solve [trm Zero, trm Op] [G] _ :-
           = (interp lp:T lp:Zero lp:Op lp:L lp:AstB) }},
   % This implements "change": there is no "cast"
   % term constructor in Coq-Elpi since a degenerate let-in can do it as well
-  P = {{ let x : lp:Ty := _ in x }}.
+  Ev = {{ let x : lp:Ty := _ in x }}.
 
 :name "error"
 solve _ _ _ :- coq.error "Not an equality / no signature provided".