From 48327426b59144f1a7181092068077c5a6df7c60 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 29 Feb 2016 10:45:31 +0100 Subject: Moving the "fix" tactic to TACTIC EXTEND. --- tactics/coretactics.ml4 | 7 +++++++ tactics/tacintern.ml | 1 - tactics/tacinterp.ml | 9 --------- tactics/tacsubst.ml | 1 - 4 files changed, 7 insertions(+), 11 deletions(-) (limited to 'tactics') diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4 index 63fb67e146..c6f59f79e3 100644 --- a/tactics/coretactics.ml4 +++ b/tactics/coretactics.ml4 @@ -192,6 +192,13 @@ TACTIC EXTEND admit [ "admit" ] -> [ Proofview.give_up ] END +(* Fix *) + +TACTIC EXTEND fix + [ "fix" natural(n) ] -> [ Proofview.V82.tactic (Tactics.fix None n) ] +| [ "fix" ident(id) natural(n) ] -> [ Proofview.V82.tactic (Tactics.fix (Some id) n) ] +END + (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *) open Tacexpr diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index cbb9db65c1..b4a595b051 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -491,7 +491,6 @@ let rec intern_atomic lf ist x = TacElim (ev,intern_constr_with_bindings_arg ist cb, Option.map (intern_constr_with_bindings ist) cbo) | TacCase (ev,cb) -> TacCase (ev,intern_constr_with_bindings_arg ist cb) - | TacFix (idopt,n) -> TacFix (Option.map (intern_ident lf ist) idopt,n) | TacMutualFix (id,n,l) -> let f (id,n,c) = (intern_ident lf ist id,n,intern_type ist c) in TacMutualFix (intern_ident lf ist id, n, List.map f l) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index d5a1215b87..f74ea4fc9b 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1749,15 +1749,6 @@ and interp_atomic ist tac : unit Proofview.tactic = in Tacticals.New.tclWITHHOLES ev named_tac sigma end } - | TacFix (idopt,n) -> - Proofview.Goal.enter { enter = begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = project gl in - let idopt = Option.map (interp_ident ist env sigma) idopt in - name_atomic ~env - (TacFix(idopt,n)) - (Proofview.V82.tactic (Tactics.fix idopt n)) - end } | TacMutualFix (id,n,l) -> (* spiwack: until the tactic is in the monad *) Proofview.Trace.name_tactic (fun () -> Pp.str"") begin diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 4a5fa9828e..f611f03684 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -146,7 +146,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with TacElim (ev,subst_glob_with_bindings_arg subst cb, Option.map (subst_glob_with_bindings subst) cbo) | TacCase (ev,cb) -> TacCase (ev,subst_glob_with_bindings_arg subst cb) - | TacFix (idopt,n) as x -> x | TacMutualFix (id,n,l) -> TacMutualFix(id,n,List.map (fun (id,n,c) -> (id,n,subst_glob_constr subst c)) l) | TacCofix idopt as x -> x -- cgit v1.2.3 From bda8b2e8f90235ca875422f211cb781068b20b3c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 29 Feb 2016 10:54:08 +0100 Subject: Moving the "cofix" tactic to TACTIC EXTEND. --- tactics/coretactics.ml4 | 8 +++++++- tactics/tacintern.ml | 1 - tactics/tacinterp.ml | 9 --------- tactics/tacsubst.ml | 1 - 4 files changed, 7 insertions(+), 12 deletions(-) (limited to 'tactics') diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4 index c6f59f79e3..27efc06cca 100644 --- a/tactics/coretactics.ml4 +++ b/tactics/coretactics.ml4 @@ -199,6 +199,13 @@ TACTIC EXTEND fix | [ "fix" ident(id) natural(n) ] -> [ Proofview.V82.tactic (Tactics.fix (Some id) n) ] END +(* Cofix *) + +TACTIC EXTEND cofix + [ "cofix" ] -> [ Proofview.V82.tactic (Tactics.cofix None) ] +| [ "cofix" ident(id) ] -> [ Proofview.V82.tactic (Tactics.cofix (Some id)) ] +END + (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *) open Tacexpr @@ -217,7 +224,6 @@ let initial_atomic () = "compute", TacReduce(Cbv Redops.all_flags,nocl); "intro", TacIntroMove(None,MoveLast); "intros", TacIntroPattern []; - "cofix", TacCofix None; ] in let iter (s, t) = Tacenv.register_ltac false false (Id.of_string s) t in diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index b4a595b051..e7545597cc 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -494,7 +494,6 @@ let rec intern_atomic lf ist x = | TacMutualFix (id,n,l) -> let f (id,n,c) = (intern_ident lf ist id,n,intern_type ist c) in TacMutualFix (intern_ident lf ist id, n, List.map f l) - | TacCofix idopt -> TacCofix (Option.map (intern_ident lf ist) idopt) | TacMutualCofix (id,l) -> let f (id,c) = (intern_ident lf ist id,intern_type ist c) in TacMutualCofix (intern_ident lf ist id, List.map f l) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index f74ea4fc9b..2a741ee367 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1764,15 +1764,6 @@ and interp_atomic ist tac : unit Proofview.tactic = Sigma.Unsafe.of_pair (tac, sigma) end } end - | TacCofix idopt -> - Proofview.Goal.enter { enter = begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = project gl in - let idopt = Option.map (interp_ident ist env sigma) idopt in - name_atomic ~env - (TacCofix (idopt)) - (Proofview.V82.tactic (Tactics.cofix idopt)) - end } | TacMutualCofix (id,l) -> (* spiwack: until the tactic is in the monad *) Proofview.Trace.name_tactic (fun () -> Pp.str"") begin diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index f611f03684..faf068bfd5 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -148,7 +148,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with | TacCase (ev,cb) -> TacCase (ev,subst_glob_with_bindings_arg subst cb) | TacMutualFix (id,n,l) -> TacMutualFix(id,n,List.map (fun (id,n,c) -> (id,n,subst_glob_constr subst c)) l) - | TacCofix idopt as x -> x | TacMutualCofix (id,l) -> TacMutualCofix (id, List.map (fun (id,c) -> (id,subst_glob_constr subst c)) l) | TacAssert (b,otac,na,c) -> -- cgit v1.2.3 From d0bc16d1a0626f4137797bbf0c91e972a0ff43ac Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 29 Feb 2016 11:05:26 +0100 Subject: Moving the "clear" tactic to TACTIC EXTEND. --- tactics/coretactics.ml4 | 10 ++++++++++ tactics/tacintern.ml | 1 - tactics/tacinterp.ml | 11 ----------- tactics/tacsubst.ml | 1 - 4 files changed, 10 insertions(+), 13 deletions(-) (limited to 'tactics') diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4 index 27efc06cca..ab97dad706 100644 --- a/tactics/coretactics.ml4 +++ b/tactics/coretactics.ml4 @@ -206,6 +206,16 @@ TACTIC EXTEND cofix | [ "cofix" ident(id) ] -> [ Proofview.V82.tactic (Tactics.cofix (Some id)) ] END +(* Clear *) + +TACTIC EXTEND clear + [ "clear" hyp_list(ids) ] -> [ + if List.is_empty ids then Tactics.keep [] + else Proofview.V82.tactic (Tactics.clear ids) + ] +| [ "clear" "-" ne_hyp_list(ids) ] -> [ Tactics.keep ids ] +END + (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *) open Tacexpr diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index e7545597cc..bea8d3469b 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -525,7 +525,6 @@ let rec intern_atomic lf ist x = let h2 = intern_quantified_hypothesis ist h2 in TacDoubleInduction (h1,h2) (* Context management *) - | TacClear (b,l) -> TacClear (b,List.map (intern_hyp ist) l) | TacClearBody l -> TacClearBody (List.map (intern_hyp ist) l) | TacMove (id1,id2) -> TacMove (intern_hyp ist id1,intern_move_location ist id2) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 2a741ee367..74121d3abe 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1881,17 +1881,6 @@ and interp_atomic ist tac : unit Proofview.tactic = (TacDoubleInduction (h1,h2)) (Elim.h_double_induction h1 h2) (* Context management *) - | TacClear (b,l) -> - Proofview.Goal.enter { enter = begin fun gl -> - let env = pf_env gl in - let sigma = project gl in - let l = interp_hyp_list ist env sigma l in - if b then name_atomic ~env (TacClear (b, l)) (Tactics.keep l) - else - (* spiwack: until the tactic is in the monad *) - let tac = Proofview.V82.tactic (fun gl -> Tactics.clear l gl) in - Proofview.Trace.name_tactic (fun () -> Pp.str"") tac - end } | TacClearBody l -> Proofview.Goal.enter { enter = begin fun gl -> let env = pf_env gl in diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index faf068bfd5..0b8dbb6e3a 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -167,7 +167,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with | TacDoubleInduction (h1,h2) as x -> x (* Context management *) - | TacClear _ as x -> x | TacClearBody l as x -> x | TacMove (id1,id2) as x -> x | TacRename l as x -> x -- cgit v1.2.3 From 7dd8c2bf4747c94be6f18d7fdd0e3b593f560a2f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 29 Feb 2016 11:20:26 +0100 Subject: Moving the "clearbody" tactic to TACTIC EXTEND. --- tactics/coretactics.ml4 | 6 ++++++ tactics/tacintern.ml | 1 - tactics/tacinterp.ml | 9 --------- tactics/tacsubst.ml | 1 - 4 files changed, 6 insertions(+), 11 deletions(-) (limited to 'tactics') diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4 index ab97dad706..b68aab621e 100644 --- a/tactics/coretactics.ml4 +++ b/tactics/coretactics.ml4 @@ -216,6 +216,12 @@ TACTIC EXTEND clear | [ "clear" "-" ne_hyp_list(ids) ] -> [ Tactics.keep ids ] END +(* Clearbody *) + +TACTIC EXTEND clearbody + [ "clearbody" ne_hyp_list(ids) ] -> [ Tactics.clear_body ids ] +END + (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *) open Tacexpr diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index bea8d3469b..9775f103f8 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -525,7 +525,6 @@ let rec intern_atomic lf ist x = let h2 = intern_quantified_hypothesis ist h2 in TacDoubleInduction (h1,h2) (* Context management *) - | TacClearBody l -> TacClearBody (List.map (intern_hyp ist) l) | TacMove (id1,id2) -> TacMove (intern_hyp ist id1,intern_move_location ist id2) | TacRename l -> diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 74121d3abe..b2f539fb97 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1881,15 +1881,6 @@ and interp_atomic ist tac : unit Proofview.tactic = (TacDoubleInduction (h1,h2)) (Elim.h_double_induction h1 h2) (* Context management *) - | TacClearBody l -> - Proofview.Goal.enter { enter = begin fun gl -> - let env = pf_env gl in - let sigma = project gl in - let l = interp_hyp_list ist env sigma l in - name_atomic ~env - (TacClearBody l) - (Tactics.clear_body l) - end } | TacMove (id1,id2) -> Proofview.Goal.enter { enter = begin fun gl -> Proofview.V82.tactic (Tactics.move_hyp (interp_hyp ist (pf_env gl) (project gl) id1) diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 0b8dbb6e3a..50730eaea1 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -167,7 +167,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with | TacDoubleInduction (h1,h2) as x -> x (* Context management *) - | TacClearBody l as x -> x | TacMove (id1,id2) as x -> x | TacRename l as x -> x -- cgit v1.2.3 From 6c4fcb156dea5a71fd227606b87333ae00aacb69 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 29 Feb 2016 11:35:34 +0100 Subject: Moving the "generalize dependent" tactic to TACTIC EXTEND. --- tactics/coretactics.ml4 | 6 ++++++ tactics/tacintern.ml | 1 - tactics/tacinterp.ml | 6 ------ tactics/tacsubst.ml | 1 - 4 files changed, 6 insertions(+), 8 deletions(-) (limited to 'tactics') diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4 index b68aab621e..5862e0f8a0 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 9775f103f8..d5f7c72ec1 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 b2f539fb97..d1a47dce5a 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 50730eaea1..36e0b4278e 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) -- cgit v1.2.3 From ae3bbff3ca2564fe24bdf3dd517c82807eae9151 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 29 Feb 2016 12:11:52 +0100 Subject: Moving the "symmetry" tactic to TACTIC EXTEND. --- tactics/coretactics.ml4 | 1 + tactics/tacintern.ml | 4 ---- tactics/tacinterp.ml | 10 ---------- tactics/tacsubst.ml | 3 --- 4 files changed, 1 insertion(+), 17 deletions(-) (limited to 'tactics') diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4 index 5862e0f8a0..55461ef7c5 100644 --- a/tactics/coretactics.ml4 +++ b/tactics/coretactics.ml4 @@ -140,6 +140,7 @@ END TACTIC EXTEND symmetry [ "symmetry" ] -> [ Tactics.intros_symmetry {onhyps=Some[];concl_occs=AllOccurrences} ] +| [ "symmetry" clause(cl) ] -> [ Tactics.intros_symmetry cl ] END (** Split *) diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index d5f7c72ec1..84df21eb81 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -555,10 +555,6 @@ let rec intern_atomic lf ist x = TacChange (Some (intern_typed_pattern ist p),intern_constr ist c, clause_app (intern_hyp_location ist) cl) - (* Equivalence relations *) - | TacSymmetry idopt -> - TacSymmetry (clause_app (intern_hyp_location ist) idopt) - (* Equality and inversion *) | TacRewrite (ev,l,cl,by) -> TacRewrite diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index d1a47dce5a..81fbcc6db6 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1974,16 +1974,6 @@ and interp_atomic ist tac : unit Proofview.tactic = end } end - (* Equivalence relations *) - | TacSymmetry c -> - Proofview.Goal.enter { enter = begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = project gl in - let cl = interp_clause ist env sigma c in - name_atomic ~env - (TacSymmetry cl) - (Tactics.intros_symmetry cl) - end } (* Equality and inversion *) | TacRewrite (ev,l,cl,by) -> diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 36e0b4278e..142a964454 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -178,9 +178,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with TacChange (Option.map (subst_glob_constr_or_pattern subst) op, subst_glob_constr subst c, cl) - (* Equivalence relations *) - | TacSymmetry _ as x -> x - (* Equality and inversion *) | TacRewrite (ev,l,cl,by) -> TacRewrite (ev, -- cgit v1.2.3 From 293222e49ff81bc1299b3822d2a8c526ca803307 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 29 Feb 2016 12:40:45 +0100 Subject: Moving the "exists" tactic to TACTIC EXTEND. --- tactics/coretactics.ml4 | 23 +++++++++++++++++++++++ tactics/tacintern.ml | 3 --- tactics/tacinterp.ml | 12 ------------ tactics/tacsubst.ml | 3 --- 4 files changed, 23 insertions(+), 18 deletions(-) (limited to 'tactics') diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4 index 55461ef7c5..2d5ce53075 100644 --- a/tactics/coretactics.ml4 +++ b/tactics/coretactics.ml4 @@ -15,6 +15,7 @@ open Misctypes open Genredexpr open Proofview.Notations +open Sigma.Notations DECLARE PLUGIN "coretactics" @@ -145,6 +146,14 @@ END (** Split *) +let rec delayed_list = function +| [] -> { Tacexpr.delayed = fun _ sigma -> Sigma.here [] sigma } +| x :: l -> + { Tacexpr.delayed = fun env sigma -> + let Sigma (x, sigma, p) = x.Tacexpr.delayed env sigma in + let Sigma (l, sigma, q) = (delayed_list l).Tacexpr.delayed env sigma in + Sigma (x :: l, sigma, p +> q) } + TACTIC EXTEND split [ "split" ] -> [ Tactics.split_with_bindings false [NoBindings] ] END @@ -165,6 +174,20 @@ TACTIC EXTEND esplit_with ] END +TACTIC EXTEND exists + [ "exists" ] -> [ Tactics.split_with_bindings false [NoBindings] ] +| [ "exists" ne_bindings_list_sep(bll, ",") ] -> [ + Tacticals.New.tclDELAYEDWITHHOLES false (delayed_list bll) (fun bll -> Tactics.split_with_bindings false bll) + ] +END + +TACTIC EXTEND eexists + [ "eexists" ] -> [ Tactics.split_with_bindings true [NoBindings] ] +| [ "eexists" ne_bindings_list_sep(bll, ",") ] -> [ + Tacticals.New.tclDELAYEDWITHHOLES true (delayed_list bll) (fun bll -> Tactics.split_with_bindings true bll) + ] +END + (** Intro *) TACTIC EXTEND intros_until diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 84df21eb81..e69d3f61e0 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -531,9 +531,6 @@ let rec intern_atomic lf ist x = intern_hyp ist id1, intern_hyp ist id2) l) - (* Constructors *) - | TacSplit (ev,bll) -> TacSplit (ev,List.map (intern_bindings ist) bll) - (* Conversion *) | TacReduce (r,cl) -> dump_glob_red_expr r; diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 81fbcc6db6..65fdecc29b 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1894,18 +1894,6 @@ and interp_atomic ist tac : unit Proofview.tactic = (Tactics.rename_hyp l) end } - (* Constructors *) - | TacSplit (ev,bll) -> - Proofview.Goal.enter { enter = begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = project gl in - let sigma, bll = List.fold_map (interp_bindings ist env) sigma bll in - let named_tac = - let tac = Tactics.split_with_bindings ev bll in - name_atomic ~env (TacSplit (ev, bll)) tac - in - Tacticals.New.tclWITHHOLES ev named_tac sigma - end } (* Conversion *) | TacReduce (r,cl) -> (* spiwack: until the tactic is in the monad *) diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 142a964454..ba9a74d05a 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -169,9 +169,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with | TacMove (id1,id2) as x -> x | TacRename l as x -> x - (* Constructors *) - | TacSplit (ev,bll) -> TacSplit (ev,List.map (subst_bindings subst) bll) - (* Conversion *) | TacReduce (r,cl) -> TacReduce (subst_redexp subst r, cl) | TacChange (op,c,cl) -> -- cgit v1.2.3 From 1397f791b1699b0f04d971465270d5b2df9a6d7f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 29 Feb 2016 13:32:39 +0100 Subject: Moving the "move" tactic to TACTIC EXTEND. --- tactics/coretactics.ml4 | 9 +++++++++ tactics/tacintern.ml | 2 -- tactics/tacinterp.ml | 5 ----- tactics/tacsubst.ml | 1 - 4 files changed, 9 insertions(+), 8 deletions(-) (limited to 'tactics') diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4 index 2d5ce53075..74d98176a4 100644 --- a/tactics/coretactics.ml4 +++ b/tactics/coretactics.ml4 @@ -194,6 +194,15 @@ TACTIC EXTEND intros_until [ "intros" "until" quantified_hypothesis(h) ] -> [ Tactics.intros_until h ] END +(** Move *) + +TACTIC EXTEND move + [ "move" hyp(id) "at" "top" ] -> [ Proofview.V82.tactic (Tactics.move_hyp id MoveFirst) ] +| [ "move" hyp(id) "at" "bottom" ] -> [ Proofview.V82.tactic (Tactics.move_hyp id MoveLast) ] +| [ "move" hyp(id) "after" hyp(h) ] -> [ Proofview.V82.tactic (Tactics.move_hyp id (MoveAfter h)) ] +| [ "move" hyp(id) "before" hyp(h) ] -> [ Proofview.V82.tactic (Tactics.move_hyp id (MoveBefore h)) ] +END + (** Revert *) TACTIC EXTEND revert diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index e69d3f61e0..a069fd7557 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -524,8 +524,6 @@ let rec intern_atomic lf ist x = let h2 = intern_quantified_hypothesis ist h2 in TacDoubleInduction (h1,h2) (* Context management *) - | TacMove (id1,id2) -> - TacMove (intern_hyp ist id1,intern_move_location ist id2) | TacRename l -> TacRename (List.map (fun (id1,id2) -> intern_hyp ist id1, diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 65fdecc29b..1a8a95158a 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1875,11 +1875,6 @@ and interp_atomic ist tac : unit Proofview.tactic = (TacDoubleInduction (h1,h2)) (Elim.h_double_induction h1 h2) (* Context management *) - | TacMove (id1,id2) -> - Proofview.Goal.enter { enter = begin fun gl -> - Proofview.V82.tactic (Tactics.move_hyp (interp_hyp ist (pf_env gl) (project gl) id1) - (interp_move_location ist (pf_env gl) (project gl) id2)) - end } | TacRename l -> Proofview.Goal.enter { enter = begin fun gl -> let env = pf_env gl in diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index ba9a74d05a..3f103a290d 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -166,7 +166,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with | TacDoubleInduction (h1,h2) as x -> x (* Context management *) - | TacMove (id1,id2) as x -> x | TacRename l as x -> x (* Conversion *) -- cgit v1.2.3