aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorfilliatr2001-04-23 14:52:51 +0000
committerfilliatr2001-04-23 14:52:51 +0000
commitbdbe617da66a314ab88eddfc796de1549359779e (patch)
treecc1288b1247f3427193f660855bb3cf57cdd08bc
parentdfba2039b7352dbcfb3858bad2d201f54d16e3e2 (diff)
un warning pas beau supprimmé
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1669 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--parsing/termast.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/termast.ml b/parsing/termast.ml
index 7b7ad5848c..18ef4b3ac2 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -219,7 +219,7 @@ let rec ast_of_raw = function
ope(tag,pred::asttomatch::asteqns)
| ROldCase (_,isrec,typopt,tm,bv) ->
- warning "Old Case syntax";
+ (* warning "Old Case syntax"; *)
ope("CASE",(ast_of_rawopt typopt)
::(ast_of_raw tm)
::(Array.to_list (Array.map ast_of_raw bv)))