From 15fd88968e181fdafa0fecf82c5a32661c0f4e7e Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 20 Sep 2005 15:29:30 +0000
Subject: [PATCH] changed ast representation of exists, now an 'exists simble
 with a lambda child is used

---
 helm/ocaml/cic_notation/grafiteParser.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/helm/ocaml/cic_notation/grafiteParser.ml b/helm/ocaml/cic_notation/grafiteParser.ml
index 65df218d4..9f07baa4a 100644
--- 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)
     ]
   ];
-- 
2.39.2