inductive type ident optional in mutcase

[helm.git] / helm / ocaml / cic_disambiguation / cicTextualParser2.ml

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 2bcbb88e8da8a984c5b29c77a4620cd5be539652..0ac43a11e4d0771a6182e22579ac0ab6e2772043 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -179,7 +179,7 @@ EXTEND
             return_term loc (CicAst.LetRec (ind_kind, defs, body))
       | outtyp = OPT [ PAREN "["; typ = term; PAREN "]" -> typ ];
         "match"; t = term;
-        SYMBOL ":"; indty = IDENT;
+        indty_ident = OPT [ SYMBOL ":"; id = IDENT -> id ];
         "with";
         PAREN "[";
         patterns = LIST0 [
@@ -188,7 +188,7 @@ EXTEND
         ] SEP SYMBOL "|";
         PAREN "]" ->
           return_term loc
-            (CicAst.Case (t, indty, outtyp, patterns))
+            (CicAst.Case (t, indty_ident, outtyp, patterns))
       | PAREN "("; t = term; PAREN ")" -> return_term loc t
       ]
     ];