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. --- intf/tacexpr.mli | 1 - parsing/g_tactic.ml4 | 2 -- printing/pptactic.ml | 1 - tactics/coretactics.ml4 | 7 +++++++ tactics/tacintern.ml | 1 - tactics/tacinterp.ml | 9 --------- tactics/tacsubst.ml | 1 - 7 files changed, 7 insertions(+), 15 deletions(-) diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 502f2db4c1..3993f1b371 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -145,7 +145,6 @@ type 'a gen_atomic_tactic_expr = ('nam * 'dtrm intro_pattern_expr located option) option | TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option | TacCase of evars_flag * 'trm with_bindings_arg - | TacFix of Id.t option * int | TacMutualFix of Id.t * int * (Id.t * int * 'trm) list | TacCofix of Id.t option | TacMutualCofix of Id.t * (Id.t * 'trm) list diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 77b7b05a39..497819b327 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -555,8 +555,6 @@ GEXTEND Gram TacAtom (!@loc, TacElim (true,cl,el)) | IDENT "case"; icl = induction_clause_list -> TacAtom (!@loc, mkTacCase false icl) | IDENT "ecase"; icl = induction_clause_list -> TacAtom (!@loc, mkTacCase true icl) - | "fix"; n = natural -> TacAtom (!@loc, TacFix (None,n)) - | "fix"; id = ident; n = natural -> TacAtom (!@loc, TacFix (Some id,n)) | "fix"; id = ident; n = natural; "with"; fd = LIST1 fixdecl -> TacAtom (!@loc, TacMutualFix (id,n,List.map mk_fix_tac fd)) | "cofix" -> TacAtom (!@loc, TacCofix None) diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 12667d0f24..fe0be9b255 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -828,7 +828,6 @@ module Make ++ pr_opt pr_eliminator cbo) | TacCase (ev,cb) -> hov 1 (primitive (with_evars ev "case") ++ spc () ++ pr_with_bindings_arg cb) - | TacFix (ido,n) -> hov 1 (primitive "fix" ++ pr_opt pr_id ido ++ pr_intarg n) | TacMutualFix (id,n,l) -> hov 1 ( primitive "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc() 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. --- intf/tacexpr.mli | 1 - parsing/g_tactic.ml4 | 2 -- printing/pptactic.ml | 2 -- tactics/coretactics.ml4 | 8 +++++++- tactics/tacintern.ml | 1 - tactics/tacinterp.ml | 9 --------- tactics/tacsubst.ml | 1 - 7 files changed, 7 insertions(+), 17 deletions(-) diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 3993f1b371..33a96150c1 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -146,7 +146,6 @@ type 'a gen_atomic_tactic_expr = | TacElim of evars_flag * 'trm with_bindings_arg * 'trm with_bindings option | TacCase of evars_flag * 'trm with_bindings_arg | TacMutualFix of Id.t * int * (Id.t * int * 'trm) list - | TacCofix of Id.t option | TacMutualCofix of Id.t * (Id.t * 'trm) list | TacAssert of bool * 'tacexpr option * diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 497819b327..6c3918be3a 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -557,8 +557,6 @@ GEXTEND Gram | IDENT "ecase"; icl = induction_clause_list -> TacAtom (!@loc, mkTacCase true icl) | "fix"; id = ident; n = natural; "with"; fd = LIST1 fixdecl -> TacAtom (!@loc, TacMutualFix (id,n,List.map mk_fix_tac fd)) - | "cofix" -> TacAtom (!@loc, TacCofix None) - | "cofix"; id = ident -> TacAtom (!@loc, TacCofix (Some id)) | "cofix"; id = ident; "with"; fd = LIST1 cofixdecl -> TacAtom (!@loc, TacMutualCofix (id,List.map mk_cofix_tac fd)) diff --git a/printing/pptactic.ml b/printing/pptactic.ml index fe0be9b255..05c3b3bf42 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -832,8 +832,6 @@ module Make hov 1 ( primitive "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc() ++ keyword "with" ++ spc () ++ prlist_with_sep spc pr_fix_tac l) - | TacCofix ido -> - hov 1 (primitive "cofix" ++ pr_opt pr_id ido) | TacMutualCofix (id,l) -> hov 1 ( primitive "cofix" ++ spc () ++ pr_id id ++ spc() 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. --- intf/tacexpr.mli | 1 - parsing/g_tactic.ml4 | 4 ---- printing/pptactic.ml | 9 --------- tactics/coretactics.ml4 | 10 ++++++++++ tactics/tacintern.ml | 1 - tactics/tacinterp.ml | 11 ----------- tactics/tacsubst.ml | 1 - test-suite/bugs/closed/3612.v | 3 +++ toplevel/vernacentries.ml | 9 +++++++-- 9 files changed, 20 insertions(+), 29 deletions(-) diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 33a96150c1..10c616627a 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -161,7 +161,6 @@ type 'a gen_atomic_tactic_expr = | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis (* Context management *) - | TacClear of bool * 'nam list | TacClearBody of 'nam list | TacMove of 'nam * 'nam move_location | TacRename of ('nam *'nam) list diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 6c3918be3a..ad5f78b46d 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -618,10 +618,6 @@ GEXTEND Gram TacAtom (!@loc, TacInductionDestruct(false,true,icl)) (* Context management *) - | IDENT "clear"; "-"; l = LIST1 id_or_meta -> TacAtom (!@loc, TacClear (true, l)) - | IDENT "clear"; l = LIST0 id_or_meta -> - let is_empty = match l with [] -> true | _ -> false in - TacAtom (!@loc, TacClear (is_empty, l)) | IDENT "clearbody"; l = LIST1 id_or_meta -> TacAtom (!@loc, TacClearBody l) | IDENT "move"; hfrom = id_or_meta; hto = move_location -> TacAtom (!@loc, TacMove (hfrom,hto)) diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 05c3b3bf42..c61b80c834 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -793,7 +793,6 @@ module Make let rec pr_atom0 a = tag_atom a (match a with | TacIntroPattern [] -> primitive "intros" | TacIntroMove (None,MoveLast) -> primitive "intro" - | TacClear (true,[]) -> primitive "clear" | t -> str "(" ++ pr_atom1 t ++ str ")" ) @@ -899,14 +898,6 @@ module Make ) (* Context management *) - | TacClear (true,[]) as t -> - pr_atom0 t - | TacClear (keep,l) -> - hov 1 ( - primitive "clear" ++ spc () - ++ (if keep then str "- " else mt ()) - ++ prlist_with_sep spc pr.pr_name l - ) | TacClearBody l -> hov 1 ( primitive "clearbody" ++ spc () 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 diff --git a/test-suite/bugs/closed/3612.v b/test-suite/bugs/closed/3612.v index 9125ab16dd..25060debe2 100644 --- a/test-suite/bugs/closed/3612.v +++ b/test-suite/bugs/closed/3612.v @@ -35,6 +35,9 @@ Axiom path_path_sigma : forall {A : Type} (P : A -> Type) (u v : sigT P) (r : p..1 = q..1) (s : transport (fun x => transport P x u.2 = v.2) r p..2 = q..2), p = q. + +Declare ML Module "coretactics". + Goal forall (A : Type) (B : forall _ : A, Type) (x : @sigT A (fun x : A => B x)) (xx : @paths (@sigT A (fun x0 : A => B x0)) x x), @paths (@paths (@sigT A (fun x0 : A => B x0)) x x) xx diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index a6a1546ae3..38832b422f 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -884,8 +884,13 @@ let vernac_set_used_variables e = (str "Unknown variable: " ++ pr_id id)) l; let _, to_clear = set_used_variables l in - vernac_solve - SelectAll None Tacexpr.(TacAtom (Loc.ghost,TacClear(false,to_clear))) false + (** FIXME: too fragile *) + let open Tacexpr in + let tac = { mltac_plugin = "coretactics"; mltac_tactic = "clear" } in + let tac = { mltac_name = tac; mltac_index = 0 } in + let arg = Genarg.in_gen (Genarg.rawwit (Genarg.wit_list Constrarg.wit_var)) to_clear in + let tac = if List.is_empty to_clear then TacId [] else TacML (Loc.ghost, tac, [TacGeneric arg]) in + vernac_solve SelectAll None tac false (*****************************) -- 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. --- intf/tacexpr.mli | 1 - parsing/g_tactic.ml4 | 1 - printing/pptactic.ml | 5 ----- tactics/coretactics.ml4 | 6 ++++++ tactics/tacintern.ml | 1 - tactics/tacinterp.ml | 9 --------- tactics/tacsubst.ml | 1 - 7 files changed, 6 insertions(+), 18 deletions(-) diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 10c616627a..d936748f2d 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -161,7 +161,6 @@ type 'a gen_atomic_tactic_expr = | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis (* Context management *) - | TacClearBody of 'nam list | TacMove of 'nam * 'nam move_location | TacRename of ('nam *'nam) list diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index ad5f78b46d..04ee02f944 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -618,7 +618,6 @@ GEXTEND Gram TacAtom (!@loc, TacInductionDestruct(false,true,icl)) (* Context management *) - | IDENT "clearbody"; l = LIST1 id_or_meta -> TacAtom (!@loc, TacClearBody l) | IDENT "move"; hfrom = id_or_meta; hto = move_location -> TacAtom (!@loc, TacMove (hfrom,hto)) | IDENT "rename"; l = LIST1 rename SEP "," -> TacAtom (!@loc, TacRename l) diff --git a/printing/pptactic.ml b/printing/pptactic.ml index c61b80c834..b1d6fb0c0f 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -898,11 +898,6 @@ module Make ) (* Context management *) - | TacClearBody l -> - hov 1 ( - primitive "clearbody" ++ spc () - ++ prlist_with_sep spc pr.pr_name l - ) | TacMove (id1,id2) -> hov 1 ( primitive "move" 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. --- intf/tacexpr.mli | 1 - parsing/g_tactic.ml4 | 1 - printing/pptactic.ml | 5 ----- tactics/coretactics.ml4 | 6 ++++++ tactics/tacintern.ml | 1 - tactics/tacinterp.ml | 6 ------ tactics/tacsubst.ml | 1 - 7 files changed, 6 insertions(+), 15 deletions(-) diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index d936748f2d..52c07e089a 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 04ee02f944..238b9a60f7 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 b1d6fb0c0f..f4007e25e1 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 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. --- intf/tacexpr.mli | 3 --- parsing/g_tactic.ml4 | 2 -- printing/pptactic.ml | 4 ---- tactics/coretactics.ml4 | 1 + tactics/tacintern.ml | 4 ---- tactics/tacinterp.ml | 10 ---------- tactics/tacsubst.ml | 3 --- 7 files changed, 1 insertion(+), 26 deletions(-) diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 52c07e089a..3f1d0fd76c 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -170,9 +170,6 @@ type 'a gen_atomic_tactic_expr = | TacReduce of ('trm,'cst,'pat) red_expr_gen * 'nam clause_expr | TacChange of 'pat option * 'dtrm * 'nam clause_expr - (* Equivalence relations *) - | TacSymmetry of 'nam clause_expr - (* Equality and inversion *) | TacRewrite of evars_flag * (bool * multi * 'dtrm with_bindings_arg) list * 'nam clause_expr * diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 238b9a60f7..4587e321f0 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -625,8 +625,6 @@ GEXTEND Gram | "exists"; bll = opt_bindings -> TacAtom (!@loc, TacSplit (false,bll)) | IDENT "eexists"; bll = opt_bindings -> TacAtom (!@loc, TacSplit (true,bll)) - (* Equivalence relations *) - | IDENT "symmetry"; "in"; cl = in_clause -> TacAtom (!@loc, TacSymmetry cl) (* Equality and inversion *) | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ","; diff --git a/printing/pptactic.ml b/printing/pptactic.ml index f4007e25e1..689ac6e4eb 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -935,10 +935,6 @@ module Make ) ++ pr.pr_dconstr c ++ pr_clauses (Some true) pr.pr_name h ) - (* Equivalence relations *) - | TacSymmetry cls -> - primitive "symmetry" ++ pr_clauses (Some true) pr.pr_name cls - (* Equality and inversion *) | TacRewrite (ev,l,cl,by) -> hov 1 ( 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. --- intf/tacexpr.mli | 3 --- parsing/g_tactic.ml4 | 5 ----- printing/pptactic.ml | 8 -------- tactics/coretactics.ml4 | 23 +++++++++++++++++++++++ tactics/tacintern.ml | 3 --- tactics/tacinterp.ml | 12 ------------ tactics/tacsubst.ml | 3 --- 7 files changed, 23 insertions(+), 34 deletions(-) diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index 3f1d0fd76c..dae960e0e5 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -163,9 +163,6 @@ type 'a gen_atomic_tactic_expr = | TacMove of 'nam * 'nam move_location | TacRename of ('nam *'nam) list - (* Trmuctors *) - | TacSplit of evars_flag * 'trm bindings list - (* Conversion *) | TacReduce of ('trm,'cst,'pat) red_expr_gen * 'nam clause_expr | TacChange of 'pat option * 'dtrm * 'nam clause_expr diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 4587e321f0..e50eca25be 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -621,11 +621,6 @@ GEXTEND Gram TacAtom (!@loc, TacMove (hfrom,hto)) | IDENT "rename"; l = LIST1 rename SEP "," -> TacAtom (!@loc, TacRename l) - (* Constructors *) - | "exists"; bll = opt_bindings -> TacAtom (!@loc, TacSplit (false,bll)) - | IDENT "eexists"; bll = opt_bindings -> - TacAtom (!@loc, TacSplit (true,bll)) - (* Equality and inversion *) | IDENT "rewrite"; l = LIST1 oriented_rewriter SEP ","; cl = clause_dft_concl; t=opt_by_tactic -> TacAtom (!@loc, TacRewrite (false,l,cl,t)) diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 689ac6e4eb..2c57cb811e 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -725,7 +725,6 @@ module Make (* some shortcuts *) let _pr_bindings = pr_bindings pr.pr_constr pr.pr_lconstr in - let pr_ex_bindings = pr_bindings_gen true pr.pr_constr pr.pr_lconstr in let pr_with_bindings = pr_with_bindings pr.pr_constr pr.pr_lconstr in let pr_with_bindings_arg_full = pr_with_bindings_arg in let pr_with_bindings_arg = pr_with_bindings_arg pr.pr_constr pr.pr_lconstr in @@ -909,13 +908,6 @@ module Make l ) - (* Constructors *) - | TacSplit (ev,l) -> - hov 1 ( - primitive (with_evars ev "exists") - ++ prlist_with_sep (fun () -> str",") pr_ex_bindings l - ) - (* Conversion *) | TacReduce (r,h) -> hov 1 ( 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. --- intf/tacexpr.mli | 1 - parsing/g_tactic.ml4 | 2 -- printing/pptactic.ml | 6 ------ tactics/coretactics.ml4 | 9 +++++++++ tactics/tacintern.ml | 2 -- tactics/tacinterp.ml | 5 ----- tactics/tacsubst.ml | 1 - 7 files changed, 9 insertions(+), 17 deletions(-) diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index dae960e0e5..7366bc03e6 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -160,7 +160,6 @@ type 'a gen_atomic_tactic_expr = | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis (* Context management *) - | TacMove of 'nam * 'nam move_location | TacRename of ('nam *'nam) list (* Conversion *) diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index e50eca25be..0c90a8bca4 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -617,8 +617,6 @@ GEXTEND Gram TacAtom (!@loc, TacInductionDestruct(false,true,icl)) (* Context management *) - | IDENT "move"; hfrom = id_or_meta; hto = move_location -> - TacAtom (!@loc, TacMove (hfrom,hto)) | IDENT "rename"; l = LIST1 rename SEP "," -> TacAtom (!@loc, TacRename l) (* Equality and inversion *) diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 2c57cb811e..36863906ea 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -892,12 +892,6 @@ module Make ) (* Context management *) - | TacMove (id1,id2) -> - hov 1 ( - primitive "move" - ++ brk (1,1) ++ pr.pr_name id1 - ++ Miscprint.pr_move_location pr.pr_name id2 - ) | TacRename l -> hov 1 ( primitive "rename" ++ brk (1,1) 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