diff options
| author | Hugo Herbelin | 2016-07-12 11:53:37 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-05-30 14:40:45 +0200 |
| commit | be73d7eccd3e3165ce719b36910920e05cf416bc (patch) | |
| tree | e4080480250a13e90fa326b92697ff524f6a35ca /tactics | |
| parent | 9a63fdf0cad004d21ff9e937b08e7758e304bcd3 (diff) | |
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.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 4 | ||||
| -rw-r--r-- | tactics/tactics.mli | 2 |
2 files changed, 3 insertions, 3 deletions
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. } *) |