diff options
| author | Pierre-Marie Pédrot | 2014-09-02 14:26:14 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-09-02 14:32:57 +0200 |
| commit | ac60d974cc028cef60eb3593d1778977c1636629 (patch) | |
| tree | 2dad4d45848cc94bf6db0997c124e91ba4145091 /tactics | |
| parent | deebdaa96867dc4424d412956b3a2f595f4d4cc7 (diff) | |
Removing [revert] tactic from the AST.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/coretactics.ml4 | 8 | ||||
| -rw-r--r-- | tactics/tacintern.ml | 1 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 5 | ||||
| -rw-r--r-- | tactics/tacsubst.ml | 1 |
4 files changed, 7 insertions, 8 deletions
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4 index d429dc07e7..a464b5e8d9 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 eac80a63a4..fd5d236567 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 8c86db6130..e69a307bdf 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 cdea2b47b9..ab96fe6748 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) |