From 9a63fdf0cad004d21ff9e937b08e7758e304bcd3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 12 Jul 2016 11:40:52 +0200
Subject: Adding "eassert", "eenough", "epose proof", which allow to state a
 goal with unresolved evars.

---
 plugins/ltac/tacsubst.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/ltac/tacsubst.ml')

diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index 4390ff08b4..1ae792971c 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -146,8 +146,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
       TacMutualFix(id,n,List.map (fun (id,n,c) -> (id,n,subst_glob_constr subst c)) l)
   | TacMutualCofix (id,l) ->
       TacMutualCofix (id, List.map (fun (id,c) -> (id,subst_glob_constr subst c)) l)
-  | TacAssert (b,otac,na,c) ->
-      TacAssert (b,Option.map (Option.map (subst_tactic subst)) otac,na,
+  | TacAssert (ev,b,otac,na,c) ->
+      TacAssert (ev,b,Option.map (Option.map (subst_tactic subst)) otac,na,
                  subst_glob_constr subst c)
   | TacGeneralize cl ->
       TacGeneralize (List.map (on_fst (subst_constr_with_occurrences subst))cl)
-- 
cgit v1.2.3


From be73d7eccd3e3165ce719b36910920e05cf416bc Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 12 Jul 2016 11:53:37 +0200
Subject: Adding "epose", "eset", "eremember" which allow to set terms with
 evars.

This is for consistency with the rest of the language. For instance,
"eremember" and "epose" are supposed to refer to terms occurring in
the goal, hence not leaving evars, hence in general pointless.

Eventually, I guess that "e" should be a modifier (see e.g. the
discussion at #3872), or the difference is removed.
---
 plugins/ltac/tacsubst.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/ltac/tacsubst.ml')

diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index 1ae792971c..f5e6f05cee 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -151,8 +151,8 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
                  subst_glob_constr subst c)
   | TacGeneralize cl ->
       TacGeneralize (List.map (on_fst (subst_constr_with_occurrences subst))cl)
-  | TacLetTac (id,c,clp,b,eqpat) ->
-    TacLetTac (id,subst_glob_constr subst c,clp,b,eqpat)
+  | TacLetTac (ev,id,c,clp,b,eqpat) ->
+    TacLetTac (ev,id,subst_glob_constr subst c,clp,b,eqpat)
 
   (* Derived basic tactics *)
   | TacInductionDestruct (isrec,ev,(l,el)) ->
-- 
cgit v1.2.3