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.

6 files changed, 34 insertions, 22 deletions

diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index c6a3beb896..83bfd0233a 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -538,16 +538,27 @@ GEXTEND Gram
 	  TacAtom (Loc.tag ~loc:!@loc @@ TacMutualCofix (id,List.map mk_cofix_tac fd))
 
       | IDENT "pose"; (id,b) = bindings_with_parameters ->
-	  TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (Names.Name id,b,Locusops.nowhere,true,None))
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,Names.Name id,b,Locusops.nowhere,true,None))
       | IDENT "pose"; b = constr; na = as_name ->
-	  TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (na,b,Locusops.nowhere,true,None))
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,na,b,Locusops.nowhere,true,None))
+      | IDENT "epose"; (id,b) = bindings_with_parameters ->
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,Names.Name id,b,Locusops.nowhere,true,None))
+      | IDENT "epose"; b = constr; na = as_name ->
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,na,b,Locusops.nowhere,true,None))
       | IDENT "set"; (id,c) = bindings_with_parameters; p = clause_dft_concl ->
-	  TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (Names.Name id,c,p,true,None))
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,Names.Name id,c,p,true,None))
       | IDENT "set"; c = constr; na = as_name; p = clause_dft_concl ->
-          TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (na,c,p,true,None))
+          TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,na,c,p,true,None))
+      | IDENT "eset"; (id,c) = bindings_with_parameters; p = clause_dft_concl ->
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,Names.Name id,c,p,true,None))
+      | IDENT "eset"; c = constr; na = as_name; p = clause_dft_concl ->
+          TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,na,c,p,true,None))
       | IDENT "remember"; c = constr; na = as_name; e = eqn_ipat;
           p = clause_dft_all ->
-          TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (na,c,p,false,e))
+          TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,na,c,p,false,e))
+      | IDENT "eremember"; c = constr; na = as_name; e = eqn_ipat;
+          p = clause_dft_all ->
+          TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,na,c,p,false,e))
 
       (* Alternative syntax for "pose proof c as id" *)
       | IDENT "assert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":=";
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 22ecf61aa2..4e254ea766 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -786,11 +786,11 @@ type 'a extra_genarg_printer =
               pr_with_occurrences pr.pr_constr cl ++ pr_as_name na)
               l
           )
-        | TacLetTac (na,c,cl,true,_) when Locusops.is_nowhere cl ->
-          hov 1 (primitive "pose" ++ pr_pose pr.pr_constr pr.pr_lconstr na c)
-        | TacLetTac (na,c,cl,b,e) ->
+        | TacLetTac (ev,na,c,cl,true,_) when Locusops.is_nowhere cl ->
+          hov 1 (primitive (if ev then "epose" else "pose") ++ pr_pose pr.pr_constr pr.pr_lconstr na c)
+        | TacLetTac (ev,na,c,cl,b,e) ->
           hov 1 (
-            (if b then primitive "set" else primitive "remember") ++
+            primitive (if b then if ev then "eset" else "set" else if ev then "eremember" else "remember") ++
               (if b then pr_pose pr.pr_constr pr.pr_lconstr na c
                 else pr_pose_as_style pr.pr_constr na c) ++
               pr_opt (fun p -> pr_eqn_ipat p ++ spc ()) e ++
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 11e7278d92..b78dc37426 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -144,7 +144,7 @@ type 'a gen_atomic_tactic_expr =
       evars_flag * bool * 'tacexpr option option *
       'dtrm intro_pattern_expr located option * 'trm
   | TacGeneralize of ('trm with_occurrences * Name.t) list
-  | TacLetTac of Name.t * 'trm * 'nam clause_expr * letin_flag *
+  | TacLetTac of evars_flag * Name.t * 'trm * 'nam clause_expr * letin_flag *
       intro_pattern_naming_expr located option
 
   (* Derived basic tactics *)
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 734ce46e48..2dc3bb3786 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -497,9 +497,9 @@ let rec intern_atomic lf ist x =
       TacGeneralize (List.map (fun (c,na) ->
 	               intern_constr_with_occurrences ist c,
                        intern_name lf ist na) cl)
-  | TacLetTac (na,c,cls,b,eqpat) ->
+  | TacLetTac (ev,na,c,cls,b,eqpat) ->
       let na = intern_name lf ist na in
-      TacLetTac (na,intern_constr ist c,
+      TacLetTac (ev,na,intern_constr ist c,
                  (clause_app (intern_hyp_location ist) cls),b,
 		 (Option.map (intern_intro_pattern_naming_loc lf ist) eqpat))
 
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index d4ed770153..6b0914ff95 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1751,36 +1751,37 @@ and interp_atomic ist tac : unit Proofview.tactic =
           (TacGeneralize cl)
           (Tactics.generalize_gen cl)) sigma
       end }
-  | TacLetTac (na,c,clp,b,eqpat) ->
+  | TacLetTac (ev,na,c,clp,b,eqpat) ->
       Proofview.Goal.enter { enter = begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = project gl in
         let clp = interp_clause ist env sigma clp in
         let eqpat = interp_intro_pattern_naming_option ist env sigma eqpat in
-        if Locusops.is_nowhere clp then
+        if Locusops.is_nowhere clp (* typically "pose" *) then
         (* We try to fully-typecheck the term *)
-          let (sigma,c_interp) = interp_constr ist env sigma c in
+          let flags = open_constr_use_classes_flags () in
+          let (sigma,c_interp) = interp_open_constr ~flags ist env sigma c in
           let let_tac b na c cl eqpat =
             let id = Option.default (Loc.tag IntroAnonymous) eqpat in
             let with_eq = if b then None else Some (true,id) in
             Tactics.letin_tac with_eq na c None cl
           in
           let na = interp_name ist env sigma na in
-          Tacticals.New.tclWITHHOLES false
+          Tacticals.New.tclWITHHOLES ev
           (name_atomic ~env
-            (TacLetTac(na,c_interp,clp,b,eqpat))
+            (TacLetTac(ev,na,c_interp,clp,b,eqpat))
             (let_tac b na c_interp clp eqpat)) sigma
         else
         (* We try to keep the pattern structure as much as possible *)
           let let_pat_tac b na c cl eqpat =
             let id = Option.default (Loc.tag IntroAnonymous) eqpat in
             let with_eq = if b then None else Some (true,id) in
-            Tactics.letin_pat_tac with_eq na c cl
+            Tactics.letin_pat_tac ev with_eq na c cl
           in
           let (sigma',c) = interp_pure_open_constr ist env sigma c in
           name_atomic ~env
-            (TacLetTac(na,c,clp,b,eqpat))
-	    (Tacticals.New.tclWITHHOLES false (*in hope of a future "eset/epose"*)
+            (TacLetTac(ev,na,c,clp,b,eqpat))
+	    (Tacticals.New.tclWITHHOLES ev
                (let_pat_tac b (interp_name ist env sigma na)
                   (sigma,c) clp eqpat) sigma')
       end }
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)) ->