From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 7 Jun 2005 15:45:19 +0000 (+0000)
Subject: changed match syntax:
X-Git-Tag: PRE_INDEX_1~57
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d5e420ba0286d6b6ccab7101bdd75a1442385e06;p=helm.git

changed match syntax:
match x in type ty_x with ...
---

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 6e368d79b..78d1bf181 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -294,7 +294,7 @@ EXTEND
             return_term loc (CicAst.Meta (index, substs))
       | outtyp = OPT [ PAREN "["; typ = term; PAREN "]" -> typ ];
         "match"; t = term;
-        indty_ident = OPT [ SYMBOL ":"; id = IDENT -> id ];
+        indty_ident = OPT ["in" ; id = IDENT -> id ];
         "with";
         PAREN "[";
         patterns = LIST0 [