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.

---
 printing/pptactic.ml | 9 ---------
 1 file changed, 9 deletions(-)

(limited to 'printing')

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 ()
-- 
cgit v1.2.3