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.
---
 tactics/tactics.ml  | 4 ++--
 tactics/tactics.mli | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'tactics')

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 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).
---
 tactics/hipattern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

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 @@
-- 
cgit v1.2.3