From 1d6eac66b4f21a768e98d01416e4ecef68ada377 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 1 Sep 2014 16:54:53 +0200
Subject: Moving the decompose tactic out of the AST.

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

(limited to 'printing')

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index a3a023ce9d..f3bec78e20 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -759,10 +759,6 @@ and pr_atom1 = function
         (str "double induction" ++
          pr_arg pr_quantified_hypothesis h1 ++
 	 pr_arg pr_quantified_hypothesis h2)
-  | TacDecompose (l,c) ->
-      hov 1 (str "decompose" ++ spc () ++
-        hov 0 (str "[" ++ prlist_with_sep spc pr_ind l
-	  ++ str "]" ++ pr_constrarg c))
   (* Automation tactics *)
   | TacTrivial (_,[],Some []) as x -> pr_atom0 x
   | TacTrivial (d,lems,db) ->
-- 
cgit v1.2.3