From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 20 Sep 2005 15:29:30 +0000 (+0000)
Subject: changed ast representation of exists, now an 'exists simble with a lambda child is... 
X-Git-Tag: LAST_BEFORE_NEW~80
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=15fd88968e181fdafa0fecf82c5a32661c0f4e7e;p=helm.git

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

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)
     ]
   ];