From 04ceaad7583afcd85754b909ae25e7128646ff54 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 21 Oct 2002 13:07:30 +0000
Subject: NewDestruct/NewInduction acceptent l'option "using"

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3167 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/tacexpr.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'proofs')

diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index b63588aaa4..3eaaea5739 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -116,9 +116,9 @@ type ('constr,'cst,'ind,'id) gen_atomic_tactic_expr =
 
   (* Derived basic tactics *)
   | TacOldInduction of quantified_hypothesis
-  | TacNewInduction of 'constr induction_arg
+  | TacNewInduction of 'constr induction_arg * 'constr with_bindings option
   | TacOldDestruct of quantified_hypothesis
-  | TacNewDestruct of 'constr induction_arg
+  | TacNewDestruct of 'constr induction_arg * 'constr with_bindings option
 
   | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis
   | TacDecomposeAnd of 'constr
-- 
cgit v1.2.3