aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-03-22 14:39:53 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-03-22 14:39:53 +0000
commita2ce571b14985a5d36d217ac86560093c71ed727 (patch)
treeb1b539ccf0c113ee04f1a1910c976f1b6145a03b /parsing
parent2e1e3f84bd88243cf370f7887cca6cbdcf5fd992 (diff)
Bug MUTCASE au lieu CASE
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1476 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
-rw-r--r--parsing/termast.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/termast.ml b/parsing/termast.ml
index 796798be9..34b6cf65b 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -228,7 +228,7 @@ let rec ast_of_raw = function
| ROldCase (_,isrec,typopt,tm,bv) ->
warning "Old Case syntax";
- ope("MUTCASE",(ast_of_rawopt typopt)
+ ope("CASE",(ast_of_rawopt typopt)
::(ast_of_raw tm)
::(Array.to_list (Array.map ast_of_raw bv)))
| RRec (_,fk,idv,tyv,bv) ->