]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_disambiguation/cicTextualParser2.ml
changed match syntax:
[helm.git] / helm / ocaml / cic_disambiguation / cicTextualParser2.ml
index 6e368d79bdbb13fd0ab4fbf7171fa765c96a057c..78d1bf181c8b99c1d14b965244eac25eacc7ebc0 100644 (file)
@@ -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 [