andrea.ma removed (superseded by match.ma)

[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 fda6d14e636eac74aefc6da73e0b6a22d7dda114..9f65555a4e80c8dc999fad607b484d55df5ef9cb 100644 (file)
--- 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 ];
@@ -552,8 +553,7 @@ EXTEND
           let name,ty = 
             match defs with
             | ((Cic.Name name,Some ty),_,_) :: _ -> name,ty
-            | ((Cic.Name name,None),_,_) :: _ -> 
-                fail loc ("No type given for " ^ name)
+            | ((Cic.Name name,None),_,_) :: _ -> name,CicAst.Implicit
             | _ -> assert false 
           in
           let body = CicAst.Ident (name,None) in