Moving the "clear" tactic to TACTIC EXTEND.

1 files changed, 0 insertions, 9 deletions

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 ()