X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FcicTextualParser2.ml;h=e267aff6a28ed9324c953f35d9f39aa535b45903;hb=6b2ff99f3f6cd0e46166bc05d06eb7421f7fda84;hp=fda6d14e636eac74aefc6da73e0b6a22d7dda114;hpb=d5c4930c5eb92a76731f6fb3c19a2a0b8c268ba0;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index fda6d14e6..e267aff6a 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -175,9 +175,10 @@ EXTEND
     [ defs = LIST1 [
         name = IDENT;
         args = LIST1 [
-          PAREN "(" ; names = LIST1 IDENT SEP SYMBOL ",";
-          ty = OPT [ SYMBOL ":"; ty = term -> ty ] ; PAREN ")" ->
-            (names, ty)
+            PAREN "(" ; names = LIST1 IDENT SEP SYMBOL ",";
+            SYMBOL ":"; ty = term; PAREN ")" ->
+              (names, Some ty)
+          | name = IDENT -> [name],None
         ];
         index_name = OPT [ IDENT "on"; idx = IDENT -> idx ];
         ty = OPT [ SYMBOL ":" ; t = term -> t ];