diff options
| -rw-r--r-- | pretyping/cases.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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" >] |