diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-16 10:16:43 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-16 10:16:43 +0000 |
| commit | edfd3f7285717efc9051e86f295e1d25ced9f241 (patch) | |
| tree | de6c497d2afaa4a18d1e043c1434dc407cfc3fb9 /pretyping | |
| parent | 436dd248125d3aca29755be16c146dd9b2732c88 (diff) | |
Suppression du warning several default clauses
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1134 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -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 c6fe2cbcb..e5483e0cf 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" >] |