changed ast representation of exists, now an 'exists simble with a lambda child is...

diff --git a/helm/ocaml/cic_notation/grafiteParser.ml b/helm/ocaml/cic_notation/grafiteParser.ml
index 65df218d4f4bf22a1f8d519bcad35f2846c839bf..9f07baa4a77f62bc83394dd43425652d2289da36 100644 (file)
--- a/helm/ocaml/cic_notation/grafiteParser.ml
+++ b/helm/ocaml/cic_notation/grafiteParser.ml
@@ -352,9 +352,8 @@ EXTEND
     ]
   ];
   argument: [
-    [ id = IDENT -> Ast.IdentArg (0, id)
-    | l = LIST1 [ SYMBOL <:unicode<eta>> (* η *) -> () ] SEP SYMBOL ".";
-      SYMBOL "."; id = IDENT ->
+    [ l = LIST0 [ SYMBOL <:unicode<eta>> (* η *); SYMBOL "." -> () ];
+      id = IDENT ->
         Ast.IdentArg (List.length l, id)
     ]
   ];