diff options
| author | Pierre-Marie Pédrot | 2016-05-16 21:41:55 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-16 22:16:36 +0200 |
| commit | b3bfa1179bc6dda1a179e0ed5bc98dccdc1b3e14 (patch) | |
| tree | dd9e7016271fdad02452aed0f8cd469305e0780e /tactics | |
| parent | a4bd166bd2119a5290276f0ded44f8186ba1ecee (diff) | |
Put the "generalize" tactic in the monad.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/eqdecide.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 18 | ||||
| -rw-r--r-- | tactics/tactics.mli | 5 |
3 files changed, 11 insertions, 14 deletions
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index 01ebaa7b72..b1d3290aac 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -64,7 +64,7 @@ let choose_noteq eqonleft = let mkBranches c1 c2 = tclTHENLIST - [Proofview.V82.tactic (generalize [c2]); + [generalize [c2]; Simple.elim c1; intros; onLastHyp Simple.case; diff --git a/tactics/tactics.ml b/tactics/tactics.ml index c3d6a65eb8..d4589154f8 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2766,14 +2766,15 @@ let generalize_dep ?(with_let=false) c gl = gl (** *) -let generalize_gen_let lconstr gl = +let generalize_gen_let lconstr = Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> let newcl, evd = - List.fold_right_i (generalize_goal gl) 0 lconstr - (Tacmach.pf_concl gl,Tacmach.project gl) + List.fold_right_i (Tacmach.New.of_old generalize_goal gl) 0 lconstr + (Tacmach.New.pf_concl gl,Tacmach.New.project gl) in - Proofview.V82.of_tactic (Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evd) - (apply_type newcl (List.map_filter (fun ((_,c,b),_) -> - if Option.is_empty b then Some c else None) lconstr))) gl + let map ((_, c, b),_) = if Option.is_empty b then Some c else None in + let tac = apply_type newcl (List.map_filter map lconstr) in + Sigma.Unsafe.of_pair (tac, evd) +end } let new_generalize_gen_let lconstr = Proofview.Goal.s_enter { s_enter = begin fun gl -> @@ -2809,11 +2810,8 @@ let generalize_gen lconstr = let new_generalize_gen lconstr = new_generalize_gen_let (List.map (fun ((occs,c),na) -> (occs,c,None),na) lconstr) - -let generalize l = - generalize_gen_let (List.map (fun c -> ((AllOccurrences,c,None),Anonymous)) l) -let new_generalize l = +let generalize l = new_generalize_gen_let (List.map (fun c -> ((AllOccurrences,c,None),Anonymous)) l) (* Faudra-t-il une version avec plusieurs args de generalize_dep ? diff --git a/tactics/tactics.mli b/tactics/tactics.mli index f730dd6c40..9d02d3f6d3 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -383,10 +383,9 @@ val letin_pat_tac : (bool * intro_pattern_naming) option -> (** {6 Generalize tactics. } *) -val generalize : constr list -> tactic -val generalize_gen : (constr Locus.with_occurrences * Name.t) list -> tactic +val generalize : constr list -> unit Proofview.tactic +val generalize_gen : (constr Locus.with_occurrences * Name.t) list -> unit Proofview.tactic -val new_generalize : constr list -> unit Proofview.tactic 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 |