diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-29 11:35:34 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-29 13:24:45 +0100 |
commit | 6c4fcb156dea5a71fd227606b87333ae00aacb69 (patch) | |
tree | a8db7db16d1cec0d6ac21118d704874e0a45000b | |
parent | 7dd8c2bf4747c94be6f18d7fdd0e3b593f560a2f (diff) |
Moving the "generalize dependent" tactic to TACTIC EXTEND.
-rw-r--r-- | intf/tacexpr.mli | 1 | ||||
-rw-r--r-- | parsing/g_tactic.ml4 | 1 | ||||
-rw-r--r-- | printing/pptactic.ml | 5 | ||||
-rw-r--r-- | tactics/coretactics.ml4 | 6 | ||||
-rw-r--r-- | tactics/tacintern.ml | 1 | ||||
-rw-r--r-- | tactics/tacinterp.ml | 6 | ||||
-rw-r--r-- | tactics/tacsubst.ml | 1 |
7 files changed, 6 insertions, 15 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index d936748f2..52c07e089 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -151,7 +151,6 @@ type 'a gen_atomic_tactic_expr = bool * 'tacexpr option * 'dtrm intro_pattern_expr located option * 'trm | TacGeneralize of ('trm with_occurrences * Name.t) list - | TacGeneralizeDep of 'trm | TacLetTac of Name.t * 'trm * 'nam clause_expr * letin_flag * intro_pattern_naming_expr located option diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 04ee02f94..238b9a60f 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -603,7 +603,6 @@ GEXTEND Gram na = as_name; l = LIST0 [","; c = pattern_occ; na = as_name -> (c,na)] -> TacAtom (!@loc, TacGeneralize (((nl,c),na)::l)) - | IDENT "generalize"; IDENT "dependent"; c = constr -> TacAtom (!@loc, TacGeneralizeDep c) (* Derived basic tactics *) | IDENT "induction"; ic = induction_clause_list -> diff --git a/printing/pptactic.ml b/printing/pptactic.ml index b1d6fb0c0..f4007e25e 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -854,11 +854,6 @@ module Make pr_with_occurrences pr.pr_constr cl ++ pr_as_name na) l ) - | TacGeneralizeDep c -> - hov 1 ( - primitive "generalize" ++ spc () ++ str "dependent" - ++ pr_constrarg c - ) | TacLetTac (na,c,cl,true,_) when Locusops.is_nowhere cl -> hov 1 (primitive "pose" ++ pr_pose pr.pr_constr pr.pr_lconstr na c) | TacLetTac (na,c,cl,b,e) -> diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4 index b68aab621..5862e0f8a 100644 --- a/tactics/coretactics.ml4 +++ b/tactics/coretactics.ml4 @@ -222,6 +222,12 @@ TACTIC EXTEND clearbody [ "clearbody" ne_hyp_list(ids) ] -> [ Tactics.clear_body ids ] END +(* Generalize dependent *) + +TACTIC EXTEND generalize_dependent + [ "generalize" "dependent" constr(c) ] -> [ Proofview.V82.tactic (Tactics.generalize_dep c) ] +END + (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *) open Tacexpr diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 9775f103f..d5f7c72ec 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -505,7 +505,6 @@ let rec intern_atomic lf ist x = TacGeneralize (List.map (fun (c,na) -> intern_constr_with_occurrences ist c, intern_name lf ist na) cl) - | TacGeneralizeDep c -> TacGeneralizeDep (intern_constr ist c) | TacLetTac (na,c,cls,b,eqpat) -> let na = intern_name lf ist na in TacLetTac (na,intern_constr ist c, diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index b2f539fb9..d1a47dce5 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1803,12 +1803,6 @@ and interp_atomic ist tac : unit Proofview.tactic = (TacGeneralize cl) (Proofview.V82.tactic (Tactics.generalize_gen cl))) sigma end } - | TacGeneralizeDep c -> - (new_interp_constr ist c) (fun c -> - name_atomic (* spiwack: probably needs a goal environment *) - (TacGeneralizeDep c) - (Proofview.V82.tactic (Tactics.generalize_dep c)) - ) | TacLetTac (na,c,clp,b,eqpat) -> Proofview.V82.nf_evar_goals <*> Proofview.Goal.nf_enter { enter = begin fun gl -> diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 50730eaea..36e0b4278 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -154,7 +154,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with TacAssert (b,Option.map (subst_tactic subst) otac,na,subst_glob_constr subst c) | TacGeneralize cl -> TacGeneralize (List.map (on_fst (subst_constr_with_occurrences subst))cl) - | TacGeneralizeDep c -> TacGeneralizeDep (subst_glob_constr subst c) | TacLetTac (id,c,clp,b,eqpat) -> TacLetTac (id,subst_glob_constr subst c,clp,b,eqpat) |