From 122503a4e0afc5ebc4e5c75c7996047d71c840e8 Mon Sep 17 00:00:00 2001
From: courtieu
Date: Thu, 6 Apr 2006 09:51:31 +0000
Subject: Enlevement de message d'erreur garbage.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8684 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tactics.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c16a0303d8..18d2d5fec3 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2051,7 +2051,6 @@ let induct_destruct_l isrec lc elim names =
 let induct_destruct isrec lc elim names = 
   assert (List.length lc > 0); (* ensured by syntax, but if called inside caml? *)
   if List.length lc = 1 then (* induction on one arg: use old mechanism *)
-    let _ = print_string "\nOne arg\n" in
     try 
       let c = List.hd lc in
       match c with
@@ -2065,7 +2064,7 @@ let induct_destruct isrec lc elim names =
 	      (new_induct_gen isrec elim names (mkVar id))
     with (* If this fails, try with new mechanism but if it fails too,
 	    then the exception is the first one. *)
-      | x -> (print_string "\nfailed\n";try induct_destruct_l isrec lc elim names with _  -> raise x)
+      | x -> (try induct_destruct_l isrec lc elim names with _  -> raise x)
   else induct_destruct_l isrec lc elim names
 
 
-- 
cgit v1.2.3