added hyperlinks on case pattern heads and outtype

[helm.git] / helm / ocaml / cic_notation / cicNotationParser.ml

diff --git a/helm/ocaml/cic_notation/cicNotationParser.ml b/helm/ocaml/cic_notation/cicNotationParser.ml
index 90324541da82ba83f4e47d0188f886188e292e68..933397067539628cda6783a576879ff0ec362dab 100644 (file)
--- 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>> (* ⇒ *);