From ac60d974cc028cef60eb3593d1778977c1636629 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 2 Sep 2014 14:26:14 +0200 Subject: Removing [revert] tactic from the AST. --- intf/tacexpr.mli | 1 - parsing/g_tactic.ml4 | 1 - printing/pptactic.ml | 2 -- tactics/coretactics.ml4 | 8 +++++++- tactics/tacintern.ml | 1 - tactics/tacinterp.ml | 5 ----- tactics/tacsubst.ml | 1 - 7 files changed, 7 insertions(+), 12 deletions(-) diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index d7237f467..e2995cfab 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -154,7 +154,6 @@ type ('trm,'pat,'cst,'ref,'nam,'lev) gen_atomic_tactic_expr = | TacClearBody of 'nam list | TacMove of bool * 'nam * 'nam move_location | TacRename of ('nam *'nam) list - | TacRevert of 'nam list (* Trmuctors *) | TacSplit of evars_flag * 'trm bindings list diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 861ac5dfd..5ffabbcf5 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -644,7 +644,6 @@ GEXTEND Gram | IDENT "move"; hfrom = id_or_meta; hto = move_location -> TacAtom (!@loc, TacMove (true,hfrom,hto)) | IDENT "rename"; l = LIST1 rename SEP "," -> TacAtom (!@loc, TacRename l) - | IDENT "revert"; l = LIST1 id_or_meta -> TacAtom (!@loc, TacRevert l) (* Constructors *) | "exists"; bll = opt_bindings -> TacAtom (!@loc, TacSplit (false,bll)) diff --git a/printing/pptactic.ml b/printing/pptactic.ml index f3bec78e2..f8eb93956 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -791,8 +791,6 @@ and pr_atom1 = function (fun (i1,i2) -> pr_ident i1 ++ spc () ++ str "into" ++ spc () ++ pr_ident i2) l) - | TacRevert l -> - hov 1 (str "revert" ++ spc () ++ prlist_with_sep spc pr_ident l) (* Constructors *) | TacSplit (ev,l) -> hov 1 (str (with_evars ev "exists") ++ prlist_with_sep (fun () -> str",") pr_ex_bindings l) diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4 index d429dc07e..a464b5e8d 100644 --- a/tactics/coretactics.ml4 +++ b/tactics/coretactics.ml4 @@ -180,6 +180,12 @@ TACTIC EXTEND intros_until [ "intros" "until" quantified_hypothesis(h) ] -> [ Tactics.intros_until h ] END +(** Revert *) + +TACTIC EXTEND revert + [ "revert" ne_hyp_list(hl) ] -> [ Tactics.revert hl ] +END + (** Simple induction / destruct *) TACTIC EXTEND simple_induction @@ -201,7 +207,7 @@ let initial_atomic () = let body = TacAtom (dloc, t) in Tacenv.register_ltac false (Id.of_string s) body in - let ans = List.iter iter + let () = List.iter iter [ "red", TacReduce(Red false,nocl); "hnf", TacReduce(Hnf,nocl); "simpl", TacReduce(Simpl None,nocl); diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index eac80a63a..fd5d23656 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -521,7 +521,6 @@ let rec intern_atomic lf ist x = TacRename (List.map (fun (id1,id2) -> intern_hyp ist id1, intern_hyp ist id2) l) - | TacRevert l -> TacRevert (List.map (intern_hyp ist) l) (* Constructors *) | TacSplit (ev,bll) -> TacSplit (ev,List.map (intern_bindings ist) bll) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 8c86db613..e69a307bd 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1944,11 +1944,6 @@ and interp_atomic ist tac : unit Proofview.tactic = interp_fresh_ident ist env (snd id2)) l) gl end - | TacRevert l -> - Proofview.Goal.raw_enter begin fun gl -> - let env = Proofview.Goal.env gl in - Tactics.revert (interp_hyp_list ist env l) - end (* Constructors *) | TacSplit (ev,bll) -> diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index cdea2b47b..ab96fe674 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -173,7 +173,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with | TacClearBody l as x -> x | TacMove (dep,id1,id2) as x -> x | TacRename l as x -> x - | TacRevert _ as x -> x (* Constructors *) | TacSplit (ev,bll) -> TacSplit (ev,List.map (subst_bindings subst) bll) -- cgit v1.2.3