X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationParser.ml;h=933397067539628cda6783a576879ff0ec362dab;hb=7efb15b93cf42eae8b34a12a327ee7213c1dbecc;hp=90324541da82ba83f4e47d0188f886188e292e68;hpb=5709e4317f5c401435afe89d24bb798284c20921;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml
index 90324541d..933397067 100644
--- a/helm/ocaml/cic_notation/cicNotationParser.ml
+++ b/helm/ocaml/cic_notation/cicNotationParser.ml
@@ -445,9 +445,9 @@ EXTEND
     ]
   ];
   match_pattern: [
-    [ id = IDENT -> id, []
+    [ id = IDENT -> id, None, []
     | LPAREN; id = IDENT; vars = LIST1 possibly_typed_name; RPAREN ->
-        id, vars
+        id, None, vars
     ]
   ];
   binder: [
@@ -578,7 +578,7 @@ EXTEND
       | s = sort -> return_term loc (Ast.Sort s)
       | outtyp = OPT [ SYMBOL "["; ty = term; SYMBOL "]" -> ty ];
         "match"; t = term;
-        indty_ident = OPT [ "in"; id = IDENT -> id ];
+        indty_ident = OPT [ "in"; id = IDENT -> id, None ];
         "with"; SYMBOL "[";
         patterns = LIST0 [
           lhs = match_pattern; SYMBOL <:unicode<Rightarrow>> (* ⇒ *);