diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-16 22:18:12 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-16 22:20:30 +0200 |
| commit | c6a16e8cc607f70f519f3ebbd5856b8ff501d782 (patch) | |
| tree | d24fbe14163d0ec94867499e2fa6b91cbbc6450f /tactics | |
| parent | b3bfa1179bc6dda1a179e0ed5bc98dccdc1b3e14 (diff) | |
Put the "generalize dependent" tactic in the monad.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 9 | ||||
| -rw-r--r-- | tactics/tactics.mli | 2 |
2 files changed, 7 insertions, 4 deletions
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. } *) |