]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/content_pres/cicNotationParser.ml
The precedence level is now an optional argument of the content to pres
[helm.git] / helm / software / components / content_pres / cicNotationParser.ml
index 02c959ef78abd300712faf1d2238aa654f1c9369..7aa4efe170cc3a52a32e9bfd2383ec06b7a5bbfc 100644 (file)
@@ -450,6 +450,7 @@ EXTEND
     [ LPAREN; id = single_arg; SYMBOL ":"; typ = term; RPAREN ->
         id, Some typ
     | arg = single_arg -> arg, None
+    | SYMBOL "_" -> Ast.Ident ("_", None), None
     ]
   ];
   match_pattern: [