diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 16 | ||||
| -rw-r--r-- | tactics/tactics.mli | 2 |
2 files changed, 7 insertions, 11 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 84d09d833..1e8082f88 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1154,10 +1154,9 @@ let tactic_infer_flags with_evar = { let onOpenInductionArg env sigma tac = function | clear_flag,ElimOnConstr f -> let (cbl, sigma') = run_delayed env sigma f in - let pending = (sigma,sigma') in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma') - (tac clear_flag (pending,cbl)) + (tac clear_flag (sigma,cbl)) | clear_flag,ElimOnAnonHyp n -> Tacticals.New.tclTHEN (intros_until_n n) @@ -1165,8 +1164,7 @@ let onOpenInductionArg env sigma tac = function (fun c -> Proofview.Goal.enter { enter = begin fun gl -> let sigma = Tacmach.New.project gl in - let pending = (sigma,sigma) in - tac clear_flag (pending,(c,NoBindings)) + tac clear_flag (sigma,(c,NoBindings)) end })) | clear_flag,ElimOnIdent (_,id) -> (* A quantified hypothesis *) @@ -1174,8 +1172,7 @@ let onOpenInductionArg env sigma tac = function (try_intros_until_id_check id) (Proofview.Goal.enter { enter = begin fun gl -> let sigma = Tacmach.New.project gl in - let pending = (sigma,sigma) in - tac clear_flag (pending,(mkVar id,NoBindings)) + tac clear_flag (sigma,(mkVar id,NoBindings)) end }) let onInductionArg tac = function @@ -1198,10 +1195,9 @@ let map_destruction_arg f sigma = function let finish_delayed_evar_resolution with_evars env sigma f = let ((c, lbind), sigma') = run_delayed env sigma f in - let pending = (sigma,sigma') in let sigma' = Sigma.Unsafe.of_evar_map sigma' in let flags = tactic_infer_flags with_evars in - let Sigma (c, sigma', _) = finish_evar_resolution ~flags env sigma' (pending,c) in + let Sigma (c, sigma', _) = finish_evar_resolution ~flags env sigma' (sigma,c) in (Sigma.to_evar_map sigma', (c, lbind)) let with_no_bindings (c, lbind) = @@ -4525,11 +4521,11 @@ let induction_destruct isrec with_evars (lc,elim) = let induction ev clr c l e = induction_gen clr true ev e - (((Evd.empty,Evd.empty),(c,NoBindings)),(None,l)) None + ((Evd.empty,(c,NoBindings)),(None,l)) None let destruct ev clr c l e = induction_gen clr false ev e - (((Evd.empty,Evd.empty),(c,NoBindings)),(None,l)) None + ((Evd.empty,(c,NoBindings)),(None,l)) None (* The registered tactic, which calls the default elimination * if no elimination constant is provided. *) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 7acfb6286..354ac50b4 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 -> - Name.t -> pending_constr -> clause -> unit Proofview.tactic + Name.t -> (evar_map * constr) -> clause -> unit Proofview.tactic (** {6 Generalize tactics. } *) |