diff options
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. } *) |