From c6a16e8cc607f70f519f3ebbd5856b8ff501d782 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 16 May 2016 22:18:12 +0200 Subject: Put the "generalize dependent" tactic in the monad. --- tactics/tactics.ml | 9 ++++++--- tactics/tactics.mli | 2 +- 2 files changed, 7 insertions(+), 4 deletions(-) (limited to 'tactics') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index d4589154f..547c36164 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2727,7 +2727,7 @@ let generalize_goal gl i ((occs,c,b),na as o) (cl,sigma) = let sigma, t = Typing.type_of env sigma c in generalize_goal_gen env sigma ids i o t cl -let generalize_dep ?(with_let=false) c gl = +let old_generalize_dep ?(with_let=false) c gl = let open Context.Named.Declaration in let env = pf_env gl in let sign = pf_hyps gl in @@ -2765,6 +2765,9 @@ let generalize_dep ?(with_let=false) c gl = Proofview.V82.of_tactic (clear (List.rev tothin'))] gl +let generalize_dep ?(with_let = false) c = + Proofview.V82.tactic (old_generalize_dep ~with_let c) + (** *) let generalize_gen_let lconstr = Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> let newcl, evd = @@ -3627,7 +3630,7 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id = Tacticals.New.tclTHENLIST [ tac; rename_hyp [(id, oldid)]; Tacticals.New.tclDO n intro; - Proofview.V82.tactic (generalize_dep ~with_let:true (mkVar oldid))] + generalize_dep ~with_let:true (mkVar oldid)] else Tacticals.New.tclTHENLIST [ tac; clear [id]; @@ -3638,7 +3641,7 @@ let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id = (Tacticals.New.tclFIRST [revert vars ; Proofview.V82.tactic (fun gl -> tclMAP (fun id -> - tclTRY (generalize_dep ~with_let:true (mkVar id))) vars gl)]) + tclTRY (Proofview.V82.of_tactic (generalize_dep ~with_let:true (mkVar id)))) vars gl)]) end } let rec compare_upto_variables x y = diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 9d02d3f6d..eb041e2a0 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -388,7 +388,7 @@ val generalize_gen : (constr Locus.with_occurrences * Name.t) list -> unit Proo val new_generalize_gen : ((occurrences * constr) * Name.t) list -> unit Proofview.tactic -val generalize_dep : ?with_let:bool (** Don't lose let bindings *) -> constr -> tactic +val generalize_dep : ?with_let:bool (** Don't lose let bindings *) -> constr -> unit Proofview.tactic (** {6 Other tactics. } *) -- cgit v1.2.3