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 6e368d79bdbb13fd0ab4fbf7171fa765c96a057c..78d1bf181c8b99c1d14b965244eac25eacc7ebc0 100644 (file)
--- 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 [