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

---
 grammar/q_coqast.ml4 | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'grammar')

diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index 67331727a..6483f66a3 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -357,9 +357,6 @@ let rec mlexpr_of_atomic_tactic = function
       >>
 
   (* Derived basic tactics *)
-  | Tacexpr.TacSimpleInductionDestruct (isrec,h) ->
-      <:expr< Tacexpr.TacSimpleInductionDestruct $mlexpr_of_bool isrec$
-                  $mlexpr_of_quantified_hypothesis h$ >>
   | Tacexpr.TacInductionDestruct (isrec,ev,l) ->
       <:expr< Tacexpr.TacInductionDestruct $mlexpr_of_bool isrec$ $mlexpr_of_bool ev$
 	$mlexpr_of_triple
-- 
cgit v1.2.3