diff options
| author | courtieu | 2006-04-06 09:51:31 +0000 |
|---|---|---|
| committer | courtieu | 2006-04-06 09:51:31 +0000 |
| commit | 122503a4e0afc5ebc4e5c75c7996047d71c840e8 (patch) | |
| tree | ce04fa5562f805ec1bbc9667d6c64dfcfe4b0be1 | |
| parent | e2b369efe7d282cc7e180f9be648335745a327f4 (diff) | |
Enlevement de message d'erreur garbage.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8684 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tactics/tactics.ml | 3 |
1 files changed, 1 insertions, 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 |