From edfd3f7285717efc9051e86f295e1d25ced9f241 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 16 Dec 2000 10:16:43 +0000
Subject: Suppression du warning several default clauses

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

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index c6fe2cbcbf..e5483e0cf4 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -328,7 +328,7 @@ let check_number_of_regular_eqns eqns =
   let n =
     List.fold_left(fun i eqn ->if is_regular eqn then i+1 else i) 0 eqns in
   match n with
-    | 0 -> warning "Found several default clauses, kept the first one"
+    | 0 -> (* warning "Found several default clauses, kept the first one" *) ()
     | 1 -> ()
     | n -> errorlabstrm "build_leaf" [<'sTR "Some clauses are redondant" >]
 
-- 
cgit v1.2.3