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/g_tactic.ml4 | 27 +++++++++++++++++++++------
 plugins/ltac/pptactic.ml  |  8 ++++----
 plugins/ltac/tacexpr.mli  |  2 +-
 plugins/ltac/tacintern.ml |  4 ++--
 plugins/ltac/tacinterp.ml | 18 +++++++++---------
 plugins/ltac/tacsubst.ml  |  4 ++--
 6 files changed, 39 insertions(+), 24 deletions(-)

diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index 1404b1c1f1..c6a3beb896 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -552,24 +552,39 @@ GEXTEND Gram
       (* Alternative syntax for "pose proof c as id" *)
       | IDENT "assert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":=";
 	  c = lconstr; ")" ->
-	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,None,Some (Loc.tag ~loc:!@loc @@IntroNaming (IntroIdentifier id)),c))
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,None,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c))
+      | IDENT "eassert"; test_lpar_id_coloneq; "("; (loc,id) = identref; ":=";
+	  c = lconstr; ")" ->
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,true,None,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c))
 
       (* Alternative syntax for "assert c as id by tac" *)
       | IDENT "assert"; test_lpar_id_colon; "("; (loc,id) = identref; ":";
 	  c = lconstr; ")"; tac=by_tactic ->
-	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,Some tac,Some (Loc.tag ~loc:!@loc @@IntroNaming (IntroIdentifier id)),c))
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,Some tac,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c))
+      | IDENT "eassert"; test_lpar_id_colon; "("; (loc,id) = identref; ":";
+	  c = lconstr; ")"; tac=by_tactic ->
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,true,Some tac,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c))
 
       (* Alternative syntax for "enough c as id by tac" *)
       | IDENT "enough"; test_lpar_id_colon; "("; (loc,id) = identref; ":";
 	  c = lconstr; ")"; tac=by_tactic ->
-	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,Some tac,Some (Loc.tag ~loc:!@loc @@IntroNaming (IntroIdentifier id)),c))
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,false,Some tac,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c))
+      | IDENT "eenough"; test_lpar_id_colon; "("; (loc,id) = identref; ":";
+	  c = lconstr; ")"; tac=by_tactic ->
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,false,Some tac,Some (Loc.tag ~loc:!@loc @@ IntroNaming (IntroIdentifier id)),c))
 
       | IDENT "assert"; c = constr; ipat = as_ipat; tac = by_tactic ->
-	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,Some tac,ipat,c))
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,Some tac,ipat,c))
+      | IDENT "eassert"; c = constr; ipat = as_ipat; tac = by_tactic ->
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,true,Some tac,ipat,c))
       | IDENT "pose"; IDENT "proof"; c = lconstr; ipat = as_ipat ->
-	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,None,ipat,c))
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,true,None,ipat,c))
+      | IDENT "epose"; IDENT "proof"; c = lconstr; ipat = as_ipat ->
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,true,None,ipat,c))
       | IDENT "enough"; c = constr; ipat = as_ipat; tac = by_tactic ->
-	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,Some tac,ipat,c))
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (false,false,Some tac,ipat,c))
+      | IDENT "eenough"; c = constr; ipat = as_ipat; tac = by_tactic ->
+	  TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,false,Some tac,ipat,c))
 
       | IDENT "generalize"; c = constr ->
 	  TacAtom (Loc.tag ~loc:!@loc @@ TacGeneralize [((AllOccurrences,c),Names.Anonymous)])
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index a001c6a2ba..22ecf61aa2 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -768,15 +768,15 @@ type 'a extra_genarg_printer =
             primitive "cofix" ++ spc () ++ pr_id id ++ spc()
             ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_cofix_tac l
           )
-        | TacAssert (b,Some tac,ipat,c) ->
+        | TacAssert (ev,b,Some tac,ipat,c) ->
           hov 1 (
-            primitive (if b then "assert" else "enough") ++
+            primitive (if b then if ev then "eassert" else "assert" else if ev then "eenough" else "enough") ++
               pr_assumption pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c ++
               pr_non_empty_arg (pr_by_tactic (pr.pr_tactic (ltactical,E))) tac
           )
-        | TacAssert (_,None,ipat,c) ->
+        | TacAssert (ev,_,None,ipat,c) ->
           hov 1 (
-            primitive "pose proof"
+            primitive (if ev then "epose proof" else "pose proof")
             ++ pr_assertion pr.pr_constr pr.pr_dconstr pr.pr_lconstr ipat c
           )
         | TacGeneralize l ->
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index bf760e7bba..11e7278d92 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -141,7 +141,7 @@ type 'a gen_atomic_tactic_expr =
   | TacMutualFix of Id.t * int * (Id.t * int * 'trm) list
   | TacMutualCofix of Id.t * (Id.t * 'trm) list
   | TacAssert of
-      bool * 'tacexpr option option *
+      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 *
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index e431a13bc2..734ce46e48 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -489,8 +489,8 @@ let rec intern_atomic lf ist x =
   | TacMutualCofix (id,l) ->
       let f (id,c) = (intern_ident lf ist id,intern_type ist c) in
       TacMutualCofix (intern_ident lf ist id, List.map f l)
-  | TacAssert (b,otac,ipat,c) ->
-      TacAssert (b,Option.map (Option.map (intern_pure_tactic ist)) otac,
+  | TacAssert (ev,b,otac,ipat,c) ->
+      TacAssert (ev,b,Option.map (Option.map (intern_pure_tactic ist)) otac,
                  Option.map (intern_intro_pattern lf ist) ipat,
                  intern_constr_gen false (not (Option.is_empty otac)) ist c)
   | TacGeneralize cl ->
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index a9ec779d11..d4ed770153 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -672,10 +672,7 @@ let pure_open_constr_flags = {
   expand_evars = false }
 
 (* Interprets an open constr *)
-let interp_open_constr ?(expected_type=WithoutTypeConstraint) ist env sigma c =
-  let flags =
-    if expected_type == WithoutTypeConstraint then open_constr_no_classes_flags ()
-    else open_constr_use_classes_flags () in
+let interp_open_constr ?(expected_type=WithoutTypeConstraint) ?(flags=open_constr_no_classes_flags ()) ist env sigma c =
   interp_gen expected_type ist false flags env sigma c
 
 let interp_pure_open_constr ist =
@@ -1727,18 +1724,21 @@ and interp_atomic ist tac : unit Proofview.tactic =
         Sigma.Unsafe.of_pair (tac, sigma)
       end }
       end
-  | TacAssert (b,t,ipat,c) ->
+  | TacAssert (ev,b,t,ipat,c) ->
       Proofview.Goal.enter { enter = begin fun gl ->
         let env = Proofview.Goal.env gl in
         let sigma = project gl in
-        let (sigma,c) = 
-          (if Option.is_empty t then interp_constr else interp_type) ist env sigma c
+        let (sigma,c) =
+          let expected_type =
+            if Option.is_empty t then WithoutTypeConstraint else IsType in
+          let flags = open_constr_use_classes_flags () in
+          interp_open_constr ~expected_type ~flags ist env sigma c
         in
         let sigma, ipat' = interp_intro_pattern_option ist env sigma ipat in
         let tac = Option.map (Option.map (interp_tactic ist)) t in
-        Tacticals.New.tclWITHHOLES false
+        Tacticals.New.tclWITHHOLES ev
         (name_atomic ~env
-          (TacAssert(b,Option.map (Option.map ignore) t,ipat,c))
+          (TacAssert(ev,b,Option.map (Option.map ignore) t,ipat,c))
           (Tactics.forward b tac ipat' c)) sigma
       end }
   | TacGeneralize cl ->
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/g_tactic.ml4 | 21 ++++++++++++++++-----
 plugins/ltac/pptactic.ml  |  8 ++++----
 plugins/ltac/tacexpr.mli  |  2 +-
 plugins/ltac/tacintern.ml |  4 ++--
 plugins/ltac/tacinterp.ml | 17 +++++++++--------
 plugins/ltac/tacsubst.ml  |  4 ++--
 tactics/tactics.ml        |  4 ++--
 tactics/tactics.mli       |  2 +-
 8 files changed, 37 insertions(+), 25 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)) ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 7e8cb4e632..f4408d4033 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2756,7 +2756,7 @@ let letin_tac with_eq id c ty occs =
     Sigma (tac, sigma, p)
   end }
 
-let letin_pat_tac with_eq id c occs =
+let letin_pat_tac with_evars with_eq id c occs =
   Proofview.Goal.s_enter { s_enter = begin fun gl ->
     let sigma = Proofview.Goal.sigma gl in
     let env = Proofview.Goal.env gl in
@@ -2765,7 +2765,7 @@ let letin_pat_tac with_eq id c occs =
     let abs = AbstractPattern (false,check,id,c,occs,false) in
     let (id,_,depdecls,lastlhyp,ccl,res) = make_abstraction env sigma ccl abs in
     let Sigma (c, sigma, p) = match res with
-    | None -> finish_evar_resolution ~flags:(tactic_infer_flags false) env sigma c
+    | None -> finish_evar_resolution ~flags:(tactic_infer_flags with_evars) env sigma c
     | Some res -> res in
     let tac =
       (letin_tac_gen with_eq (id,depdecls,lastlhyp,ccl,c) None)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 07a8035427..0dbcce02c5 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -385,7 +385,7 @@ val letin_tac : (bool * intro_pattern_naming) option ->
 
 (** Common entry point for user-level "set", "pose" and "remember" *)
 
-val letin_pat_tac : (bool * intro_pattern_naming) option ->
+val letin_pat_tac : evars_flag -> (bool * intro_pattern_naming) option ->
   Name.t -> (evar_map * constr) -> clause -> unit Proofview.tactic
 
 (** {6 Generalize tactics. } *)
-- 
cgit v1.2.3


From 3074967fd01acc5987eb2ea648fcfe32aeca1749 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 12 Jul 2016 12:27:53 +0200
Subject: Few tests for e-variants of assert, set, remember.

---
 test-suite/success/forward.v | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)
 create mode 100644 test-suite/success/forward.v

diff --git a/test-suite/success/forward.v b/test-suite/success/forward.v
new file mode 100644
index 0000000000..0ed5b524f3
--- /dev/null
+++ b/test-suite/success/forward.v
@@ -0,0 +1,18 @@
+(* Testing forward reasoning *)
+
+Goal 0=0.
+Fail assert (_ = _).
+eassert (_ = _)by reflexivity.
+eassumption.
+Qed.
+
+Goal 0=0.
+Fail set (S ?[nl]).
+eset (S ?[n]).
+remember (S ?n) as x.
+instantiate (n:=0).
+Fail remember (S (S _)).
+eremember (S (S ?[x])).
+instantiate (x:=0).
+reflexivity.
+Qed.
-- 
cgit v1.2.3


From 5a86aabf4375b5f6f205dd328454748d2bc1217f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 3 Mar 2017 14:12:29 +0100
Subject: Documentation for eassert, eenough, epose proof, eset, eremember,
 epose.

Includes fixes and suggestions from Théo.
---
 CHANGES                   |  4 ++++
 doc/refman/RefMan-tac.tex | 47 +++++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 51 insertions(+)

diff --git a/CHANGES b/CHANGES
index 30bea7a7b5..8fd71f9247 100644
--- a/CHANGES
+++ b/CHANGES
@@ -26,6 +26,10 @@ Tactics
   now uses type classes and rejects terms with unresolved holes, like
   entry "constr" does. To get the former behavior use
   "open_constr_with_bindings" (possible source of incompatibility.
+- New e-variants eassert, eenough, epose proof, eset, eremember, epose
+  which behave like the corresponding variants with no "e" but turn
+  unresolved implicit arguments into existential variables, on the
+  shelf, rather than failing.
 
 Vernacular Commands
 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index fc3fdd0025..def42955ff 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1155,6 +1155,15 @@ Section~\ref{Occurrences_clauses}.
 
   These are the general forms that combine the previous possibilities.
 
+\item {\tt eset ( {\ident$_0$} \nelistnosep{\binder} := {\term} ) in {\occgoalset}}\tacindex{eset}\\
+      {\tt eset {\term} in {\occgoalset}}
+
+  While the different variants of \texttt{set} expect that no
+  existential variables are generated by the tactic, \texttt{eset}
+  removes this constraint. In practice, this is relevant only when
+  \texttt{eset} is used as a synonym of \texttt{epose}, i.e. when the
+  term does not occur in the goal.
+
 \item {\tt remember {\term} as {\ident}}\tacindex{remember}
 
   This behaves as {\tt set ( {\ident} := {\term} ) in *} and using a
@@ -1170,6 +1179,15 @@ Section~\ref{Occurrences_clauses}.
   This is a more general form of {\tt remember} that remembers the
   occurrences of {\term} specified by an occurrences set.
 
+\item
+  {\tt eremember {\term} as {\ident}}\tacindex{eremember}\\
+  {\tt eremember {\term} as {\ident} in {\occgoalset}}\\
+  {\tt eremember {\term} as {\ident} eqn:{\ident}}
+
+  While the different variants of \texttt{remember} expect that no
+  existential variables are generated by the tactic, \texttt{eremember}
+  removes this constraint.
+
 \item {\tt pose ( {\ident} := {\term} )}\tacindex{pose}
 
   This adds the local definition {\ident} := {\term} to the current
@@ -1187,6 +1205,14 @@ Section~\ref{Occurrences_clauses}.
   This behaves as {\tt pose ( {\ident} := {\term} )} but
   {\ident} is generated by {\Coq}.
 
+\item {\tt epose ( {\ident} := {\term} )}\tacindex{epose}\\
+      {\tt epose ( {\ident} \nelistnosep{\binder} := {\term} )}\\
+      {\tt epose {\term}}
+
+  While the different variants of \texttt{pose} expect that no
+  existential variables are generated by the tactic, \texttt{epose}
+  removes this constraint.
+
 \end{Variants}
 
 \subsection{\tt decompose [ {\qualid$_1$} \dots\ {\qualid$_n$} ] \term}
@@ -1284,6 +1310,14 @@ in the list of subgoals remaining to prove.
 
   \ErrMsg \errindex{Variable {\ident} is already declared}
 
+\item \texttt{eassert {\form} as {\intropattern} by {\tac}}\tacindex{eassert}\tacindex{eassert as}\tacindex{eassert by}\\
+  {\tt assert ( {\ident} := {\term} )}
+
+  While the different variants of \texttt{assert} expect that no
+  existential variables are generated by the tactic, \texttt{eassert}
+  removes this constraint. This allows not to specify the asserted
+  statement completely before starting to prove it.
+
 \item \texttt{pose proof {\term} \zeroone{as {\intropattern}}\tacindex{pose proof}}
 
   This tactic behaves like \texttt{assert T \zeroone{as {\intropattern}} by
@@ -1294,6 +1328,11 @@ in the list of subgoals remaining to prove.
     as {\intropattern}} is the same as applying
   the {\intropattern} to {\term}.
 
+\item \texttt{epose proof {\term} \zeroone{as {\intropattern}}\tacindex{epose proof}}
+
+  While \texttt{pose proof} expects that no existential variables are generated by the tactic,
+  \texttt{epose proof} removes this constraint.
+
 \item \texttt{enough ({\ident} :\ {\form})}\tacindex{enough}
 
   This adds a new hypothesis of name {\ident} asserting {\form} to the
@@ -1320,6 +1359,14 @@ in the list of subgoals remaining to prove.
   destructed. If the \texttt{as} {\intropattern} clause generates more
   than one subgoal, {\tac} is applied to all of them.
 
+\item \texttt{eenough ({\ident} :\ {\form}) by {\tac}}\tacindex{eenough}\tacindex{eenough as}\tacindex{eenough by}\\
+ \texttt{eenough {\form} by {\tac}}\tacindex{enough by}\\
+ \texttt{eenough {\form} as {\intropattern} by {\tac}}
+
+  While the different variants of \texttt{enough} expect that no
+  existential variables are generated by the tactic, \texttt{eenough}
+  removes this constraint.
+
 \item {\tt cut {\form}}\tacindex{cut}
 
   This tactic applies to any goal. It implements the non-dependent
-- 
cgit v1.2.3


From bbde815f8108f4641f5411d03f7a88096cc2221b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 24 May 2017 21:55:21 +0200
Subject: Support for using type information to infer more precise evar
 sources.

This allows a better control on the name to give to an evar and, in
particular, to address the issue about naming produced by "epose
proof" in one of the comment of Zimmi48 at PR #248 (see file names.v).

Incidentally updating output of Show output test (evar numbers shifted).
---
 engine/evarutil.ml              |   4 ++--
 engine/evarutil.mli             |   2 +-
 engine/evd.ml                   |   3 ++-
 engine/evd.mli                  |   2 +-
 engine/proofview.ml             |   6 ++++++
 engine/termops.ml               |   1 +
 interp/constrintern.ml          |  12 ++++++------
 intf/evar_kinds.mli             |   2 +-
 plugins/ltac/extratactics.ml4   |   6 +++---
 pretyping/cases.ml              |   8 ++++----
 pretyping/coercion.ml           |   8 ++++----
 pretyping/pretyping.ml          |  16 ++++++++++++++++
 tactics/hipattern.ml            |   2 +-
 test-suite/.csdp.cache          | Bin 89077 -> 89077 bytes
 test-suite/output/Show.out      |   6 +++---
 test-suite/output/inference.out |  10 +++++-----
 test-suite/output/inference.v   |   2 +-
 test-suite/output/names.out     |   6 ++++++
 test-suite/output/names.v       |   4 ++++
 test-suite/success/Abstract.v   |   1 -
 vernac/command.ml               |   2 +-
 vernac/obligations.ml           |   2 +-
 22 files changed, 69 insertions(+), 36 deletions(-)

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 6cba6f6075..3ef725cbbd 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -367,10 +367,10 @@ let push_rel_context_to_named_context env sigma typ =
 
 let default_source = Loc.tag @@ Evar_kinds.InternalHole
 
-let restrict_evar evd evk filter candidates =
+let restrict_evar evd evk filter ?src candidates =
   let evd = Sigma.to_evar_map evd in
   let candidates = Option.map (fun l -> List.map EConstr.Unsafe.to_constr l) candidates in
-  let evd, evk' = Evd.restrict evk filter ?candidates evd in
+  let evd, evk' = Evd.restrict evk filter ?candidates ?src evd in
   Sigma.Unsafe.of_pair (evk', Evd.declare_future_goal evk' evd)
 
 let new_pure_evar_full evd evi =
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index fcc435a2ec..496ec5bc43 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -57,7 +57,7 @@ val new_Type : ?rigid:rigid -> env -> 'r Sigma.t -> (constr, 'r) Sigma.sigma
 val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr
 
 val restrict_evar : 'r Sigma.t -> existential_key -> Filter.t ->
-  constr list option -> (existential_key, 'r) Sigma.sigma
+  ?src:Evar_kinds.t Loc.located -> constr list option -> (existential_key, 'r) Sigma.sigma
 
 (** Polymorphic constants *)
 
diff --git a/engine/evd.ml b/engine/evd.ml
index b677705bc9..48fceae9ec 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -653,12 +653,13 @@ let define evk body evd =
   let evar_names = EvNames.remove_name_defined evk evd.evar_names in
   { evd with defn_evars; undf_evars; last_mods; evar_names }
 
-let restrict evk filter ?candidates evd =
+let restrict evk filter ?candidates ?src evd =
   let evk' = new_untyped_evar () in
   let evar_info = EvMap.find evk evd.undf_evars in
   let evar_info' =
     { evar_info with evar_filter = filter;
       evar_candidates = candidates;
+      evar_source = (match src with None -> evar_info.evar_source | Some src -> src);
       evar_extra = Store.empty } in
   let last_mods = match evd.conv_pbs with
   | [] ->  evd.last_mods
diff --git a/engine/evd.mli b/engine/evd.mli
index 0053324706..86755c360b 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -240,7 +240,7 @@ val evars_reset_evd  : ?with_conv_pbs:bool -> ?with_univs:bool ->
 (** {6 Misc} *)
 
 val restrict : evar -> Filter.t -> ?candidates:constr list ->
-  evar_map -> evar_map * evar
+  ?src:Evar_kinds.t located -> evar_map -> evar_map * evar
 (** Restrict an undefined evar into a new evar by filtering context and
     possibly limiting the instances to a set of candidates *)
 
diff --git a/engine/proofview.ml b/engine/proofview.ml
index ddfc0e39dd..29bb1ef397 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -696,6 +696,12 @@ let mark_in_evm ~goal evd content =
   let info =
     if goal then
       { info with Evd.evar_source = match info.Evd.evar_source with
+            (* Two kinds for goal evars:
+               - GoalEvar (morally not dependent)
+               - VarInstance (morally dependent of some name).
+               This is a heuristic for naming these evars. *)
+            | loc, (Evar_kinds.QuestionMark (_,Names.Name id) |
+                    Evar_kinds.ImplicitArg (_,(_,Some id),_)) -> loc, Evar_kinds.VarInstance id
             | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x
             | loc,_ -> loc,Evar_kinds.GoalEvar }
     else info
diff --git a/engine/termops.ml b/engine/termops.ml
index ca32c06a75..1ec2b81039 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -112,6 +112,7 @@ let pr_evar_suggested_name evk sigma =
   | None -> match evi.evar_source with
   | _,Evar_kinds.ImplicitArg (c,(n,Some id),b) -> id
   | _,Evar_kinds.VarInstance id -> id
+  | _,Evar_kinds.QuestionMark (_,Name id) -> id
   | _,Evar_kinds.GoalEvar -> Id.of_string "Goal"
   | _ ->
       let env = reset_with_named_context evi.evar_hyps (Global.env()) in
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 4dcf287efc..6514ad8be5 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1081,8 +1081,8 @@ let sort_fields ~complete loc fields completer =
           let rec build_proj_list projs proj_kinds idx ~acc_first_idx acc =
             match projs with
               | [] -> (idx, acc_first_idx, acc)
-              | (Some name) :: projs ->
-                 let field_glob_ref = ConstRef name in
+              | (Some field_glob_id) :: projs ->
+                 let field_glob_ref = ConstRef field_glob_id in
                  let first_field = eq_gr field_glob_ref first_field_glob_ref in
                  begin match proj_kinds with
                     | [] -> anomaly (Pp.str "Number of projections mismatch")
@@ -1099,7 +1099,7 @@ let sort_fields ~complete loc fields completer =
                          build_proj_list projs proj_kinds idx ~acc_first_idx acc
                        else
                          build_proj_list projs proj_kinds (idx+1) ~acc_first_idx
-                                         ((idx, field_glob_ref) :: acc)
+                                         ((idx, field_glob_id) :: acc)
                  end
               | None :: projs ->
                  if complete then
@@ -1121,7 +1121,7 @@ let sort_fields ~complete loc fields completer =
                  user_err ?loc:(loc_of_reference field_ref) ~hdr:"intern"
                                (str "The field \"" ++ pr_reference field_ref ++ str "\" does not exist.") in
                let remaining_projs, (field_index, _) =
-                 let the_proj (idx, glob_ref) = eq_gr field_glob_ref glob_ref in
+                 let the_proj (idx, glob_id) = eq_gr field_glob_ref (ConstRef glob_id) in
                  try CList.extract_first the_proj remaining_projs
                  with Not_found ->
                    user_err ?loc 
@@ -1646,7 +1646,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
        let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
        let fields =
 	 sort_fields ~complete:true loc fs
-	             (fun _idx -> CAst.make ?loc @@ CHole (Some (Evar_kinds.QuestionMark st),
+	             (fun _idx -> CAst.make ?loc @@ CHole (Some (Evar_kinds.QuestionMark (st,Anonymous)),
                                                            Misctypes.IntroAnonymous, None))
        in
        begin
@@ -1726,7 +1726,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
            let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in
            (match naming with
            | Misctypes.IntroIdentifier id -> Evar_kinds.NamedHole id
-           | _ -> Evar_kinds.QuestionMark st)
+           | _ -> Evar_kinds.QuestionMark (st,Anonymous))
         | Some k -> k
         in
         let solve = match solve with
diff --git a/intf/evar_kinds.mli b/intf/evar_kinds.mli
index 470ad2a23b..835e94c777 100644
--- a/intf/evar_kinds.mli
+++ b/intf/evar_kinds.mli
@@ -21,7 +21,7 @@ type t =
      * bool (** Force inference *)
   | BinderType of Name.t
   | NamedHole of Id.t (* coming from some ?[id] syntax *)
-  | QuestionMark of obligation_definition_status
+  | QuestionMark of obligation_definition_status * Name.t
   | CasesType of bool (* true = a subterm of the type *)
   | InternalHole
   | TomatchTypeParameter of inductive * int
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index d68139a4b4..cba9c13648 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -636,7 +636,7 @@ let subst_var_with_hole occ tid t =
            else
 	     (incr locref;
               CAst.make ~loc:(Loc.make_loc (!locref,0)) @@
-	      GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true),
+	      GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),
                      Misctypes.IntroAnonymous, None)))
         else x
     | c -> map_glob_constr_left_to_right substrec c in
@@ -648,13 +648,13 @@ let subst_hole_with_term occ tc t =
   let locref = ref 0 in
   let occref = ref occ in
   let rec substrec = function
-    | { CAst.v = GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s) } ->
+    | { CAst.v = GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s) } ->
         decr occref;
         if Int.equal !occref 0 then tc
         else
 	  (incr locref;
            CAst.make ~loc:(Loc.make_loc (!locref,0)) @@
-	   GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true),Misctypes.IntroAnonymous,s))
+	   GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s))
     | c -> map_glob_constr_left_to_right substrec c
   in
   substrec t
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index c2c8065a98..4261573725 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -2064,8 +2064,8 @@ let mk_JMeq evdref typ x typ' y =
 let mk_JMeq_refl evdref typ x = 
   papp evdref coq_JMeq_refl [| typ; x |]
 
-let hole = CAst.make @@
-  GHole (Evar_kinds.QuestionMark (Evar_kinds.Define false),
+let hole na = CAst.make @@
+  GHole (Evar_kinds.QuestionMark (Evar_kinds.Define false,na),
          Misctypes.IntroAnonymous, None)
 
 let constr_of_pat env evdref arsign pat avoid =
@@ -2168,7 +2168,7 @@ let vars_of_ctx sigma ctx =
 	    prev,
 	    (CAst.make @@ GApp (
 		(CAst.make @@ GRef (delayed_force coq_eq_refl_ref, None)), 
-		   [hole; CAst.make @@ GVar prev])) :: vars
+		   [hole na; CAst.make @@ GVar prev])) :: vars
 	| _ ->
 	    match RelDecl.get_name decl with
 		Anonymous -> invalid_arg "vars_of_ctx"
@@ -2301,7 +2301,7 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity =
 	       | l  -> CAst.make @@ GApp (bref, l)
 	 in
 	 let branch = match ineqs with
-	     Some _ -> CAst.make @@ GApp (branch, [ hole ])
+	     Some _ -> CAst.make @@ GApp (branch, [ hole Anonymous ])
 	   | None -> branch
 	 in
 	 incr i;
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 3ef17912f7..83c26058ac 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -90,8 +90,8 @@ let inh_pattern_coerce_to ?loc env pat ind1 ind2 =
 
 open Program
 
-let make_existential ?loc ?(opaque = not (get_proofs_transparency ()))  env evdref c =
-  let src = Loc.tag ?loc (Evar_kinds.QuestionMark (Evar_kinds.Define opaque)) in
+let make_existential ?loc ?(opaque = not (get_proofs_transparency ())) na env evdref c =
+  let src = Loc.tag ?loc (Evar_kinds.QuestionMark (Evar_kinds.Define opaque,na)) in
   Evarutil.e_new_evar env evdref ~src c
 
 let app_opt env evdref f t =
@@ -181,7 +181,7 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr)
 		let args = List.rev (restargs @ mkRel 1 :: List.map (lift 1) tele) in
 		let pred = mkLambda (n, eqT, applist (lift 1 c, args)) in
 		let eq = papp evdref coq_eq_ind [| eqT; hdx; hdy |] in
-		let evar = make_existential ?loc env evdref eq in
+		let evar = make_existential ?loc n env evdref eq in
 		let eq_app x = papp evdref coq_eq_rect
 		  [| eqT; hdx; pred; x; hdy; evar|] 
 		in
@@ -324,7 +324,7 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr)
 	    Some
 	      (fun x ->
 		 let cx = app_opt env evdref c x in
-		 let evar = make_existential ?loc env evdref (mkApp (p, [| cx |]))
+		 let evar = make_existential ?loc Anonymous env evdref (mkApp (p, [| cx |]))
 		 in
 		   (papp evdref sig_intro [| u; p; cx; evar |]))
 	| None ->
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index e72394fa28..b0663af70c 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -383,6 +383,21 @@ let process_inference_flags flags env initial_sigma (sigma,c) =
   let c = if flags.expand_evars then nf_evar sigma c else c in
   sigma,c
 
+let adjust_evar_source evdref na c =
+  match na, kind !evdref c with
+  | Name id, Evar (evk,args) ->
+     let evi = Evd.find !evdref evk in
+     begin match evi.evar_source with
+     | loc, Evar_kinds.QuestionMark (b,Anonymous) ->
+        let src = (loc,Evar_kinds.QuestionMark (b,na)) in
+        let sigma = Sigma.Unsafe.of_evar_map !evdref in
+        let Sigma (evk', evd, _) = restrict_evar sigma evk (evar_filter evi) ~src None in
+        evdref := Sigma.to_evar_map evd;
+        mkEvar (evk',args)
+     | _ -> c
+     end
+  | _, _ -> c
+
 (* Allow references to syntactically nonexistent variables (i.e., if applied on an inductive) *)
 let allow_anonymous_refs = ref false
 
@@ -785,6 +800,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 		  args, nf_evar !evdref (j_val hj)
 		else [], j_val hj
 	    in
+            let ujval = adjust_evar_source evdref na ujval in
 	    let value, typ = app_f n (j_val resj) ujval, subst1 ujval c2 in
 	    let j = { uj_val = value; uj_type = typ } in
 	      apply_rec env (n+1) j candargs rest
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index fd5eabe648..35fbec5a6d 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -254,7 +254,7 @@ open Evar_kinds
 let mkPattern c = snd (Patternops.pattern_of_glob_constr c)
 let mkGApp f args = CAst.make @@ GApp (f, args)
 let mkGHole = CAst.make @@
-  GHole (QuestionMark (Define false), Misctypes.IntroAnonymous, None)
+  GHole (QuestionMark (Define false,Anonymous), Misctypes.IntroAnonymous, None)
 let mkGProd id c1 c2 = CAst.make @@
   GProd (Name (Id.of_string id), Explicit, c1, c2)
 let mkGArrow c1 c2 = CAst.make @@
diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache
index b99d80e95f..ba85286dd3 100644
Binary files a/test-suite/.csdp.cache and b/test-suite/.csdp.cache differ
diff --git a/test-suite/output/Show.out b/test-suite/output/Show.out
index bf1bf2809d..8acfed5d00 100644
--- a/test-suite/output/Show.out
+++ b/test-suite/output/Show.out
@@ -1,12 +1,12 @@
-3 subgoals (ID 29)
+3 subgoals (ID 31)
   
   H : 0 = 0
   ============================
   1 = 1
 
-subgoal 2 (ID 33) is:
+subgoal 2 (ID 35) is:
  1 = S (S m')
-subgoal 3 (ID 20) is:
+subgoal 3 (ID 22) is:
  S (S n') = S m
 
 (dependent evars: (printing disabled) )
diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out
index c70467912f..d28ee42761 100644
--- a/test-suite/output/inference.out
+++ b/test-suite/output/inference.out
@@ -6,13 +6,13 @@ fun e : option L => match e with
      : option L -> option L
 fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H
      : forall m n p : nat, S m <= S n + p -> m <= n + p
-fun n : nat => let x : T n := A n in ?t ?y : T n
+fun n : nat => let y : T n := A n in ?t ?x : T n
      : forall n : nat, T n
 where
-?t : [n : nat  x := A n : T n |- ?T -> T n] 
-?y : [n : nat  x := A n : T n |- ?T] 
-fun n : nat => ?t ?y : T n
+?t : [n : nat  y := A n : T n |- ?T -> T n] 
+?x : [n : nat  y := A n : T n |- ?T] 
+fun n : nat => ?t ?x : T n
      : forall n : nat, T n
 where
 ?t : [n : nat |- ?T -> T n] 
-?y : [n : nat |- ?T] 
+?x : [n : nat |- ?T] 
diff --git a/test-suite/output/inference.v b/test-suite/output/inference.v
index 1825db1676..f761a4dc5a 100644
--- a/test-suite/output/inference.v
+++ b/test-suite/output/inference.v
@@ -27,5 +27,5 @@ Check (fun m n p (H : S m <= (S n) + p) => le_S_n _ _ H).
 (* Note: exact numbers of evars are not important... *)
 
 Inductive T (n:nat) : Type := A : T n.
-Check fun n (x:=A n:T n) => _ _ : T n.
+Check fun n (y:=A n:T n) => _ _ : T n.
 Check fun n => _ _ : T n.
diff --git a/test-suite/output/names.out b/test-suite/output/names.out
index 9471b892dd..48be63a46a 100644
--- a/test-suite/output/names.out
+++ b/test-suite/output/names.out
@@ -3,3 +3,9 @@ In environment
 y : nat
 The term "a y" has type "{y0 : nat | y = y0}"
 while it is expected to have type "{x : nat | x = y}".
+1 focused subgoal
+(shelved: 1)
+  
+  H : ?n <= 3 -> 3 <= ?n -> ?n = 3
+  ============================
+  True
diff --git a/test-suite/output/names.v b/test-suite/output/names.v
index b3b5071a03..f1efd0df2a 100644
--- a/test-suite/output/names.v
+++ b/test-suite/output/names.v
@@ -3,3 +3,7 @@
 
 Parameter a : forall x, {y:nat|x=y}.
 Fail Definition b y : {x:nat|x=y} := a y.
+
+Goal (forall n m, n <= m -> m <= n -> n = m) -> True.
+intro H; epose proof (H _ 3) as H.
+Show.
diff --git a/test-suite/success/Abstract.v b/test-suite/success/Abstract.v
index ffd50f6efd..69dc9aca78 100644
--- a/test-suite/success/Abstract.v
+++ b/test-suite/success/Abstract.v
@@ -1,4 +1,3 @@
-
 (* Cf coqbugs #546 *)
 
 Require Import Omega.
diff --git a/vernac/command.ml b/vernac/command.ml
index e2ebb4d7fb..25dd724af8 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -1062,7 +1062,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
     mkApp (EConstr.of_constr (Universes.constr_of_global (delayed_force fix_sub_ref)),
 	  [| argtyp ; wf_rel ;
 	     Evarutil.e_new_evar env evdref
-	       ~src:(Loc.tag @@ Evar_kinds.QuestionMark (Evar_kinds.Define false)) wf_proof;
+	       ~src:(Loc.tag @@ Evar_kinds.QuestionMark (Evar_kinds.Define false,Anonymous)) wf_proof;
 	     prop |])
   in
   let def = Typing.e_solve_evars env evdref def in
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index be58c67a9e..47ac16f9c7 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -221,7 +221,7 @@ let eterm_obligations env name evm fs ?status t ty =
 	 in
 	 let loc, k = evar_source id evm in
 	 let status = match k with
-           | Evar_kinds.QuestionMark o -> o
+           | Evar_kinds.QuestionMark (o,_) -> o
            | _ -> match status with
                  | Some o -> o
                  | None -> Evar_kinds.Define (not (Program.get_proofs_transparency ()))
-- 
cgit v1.2.3