From 876f202985d5bd463bd5b44c195b239bcfedad7c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 7 Aug 2014 01:43:37 +0200
Subject: Removing simple induction / destruct from the AST.

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

(limited to 'printing')

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index cdcff9bb2c..42a7e894a1 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -721,9 +721,6 @@ and pr_atom1 = function
 	     ++ str "in" ++ pr_hyp_location pr_ident (id,[],(hloc,ref None)))
 *)
   (* Derived basic tactics *)
-  | TacSimpleInductionDestruct (isrec,h) ->
-      hov 1 (str "simple " ++ str (if isrec then "induction" else "destruct")
-             ++ pr_arg pr_quantified_hypothesis h)
   | TacInductionDestruct (isrec,ev,(l,el,cl)) ->
       hov 1 (str (with_evars ev (if isrec then "induction" else "destruct")) ++
              spc () ++
-- 
cgit v1.2.3