From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 20 Apr 2005 16:12:01 +0000 (+0000)
Subject: changed binding strength of some parsing entries:
X-Git-Tag: after_svn_merge~33
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=89c46fa15cd1dd1c9b180e569a27df490c28443d;p=helm.git

changed binding strength of some parsing entries:
( a > b means a binds more tightly than b)
- now: infix operators > binders > application
- previous: application > infix operators > binders
---

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index d5f427c4f..445871045 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -225,6 +225,14 @@ EXTEND
         defs = let_defs; "in"; body = term ->
             return_term loc (CicAst.LetRec (ind_kind, defs, body))
       ]
+    | "apply" LEFTA
+      [ t1 = term; t2 = term ->
+        let rec aux = function
+          | CicAst.Appl (hd :: tl) -> aux hd @ tl
+          | term -> [term]
+        in
+        CicAst.Appl (aux t1 @ [t2])
+      ]
     | "binder" RIGHTA
       [
         b = binder;
@@ -258,14 +266,6 @@ EXTEND
     | "mult" LEFTA    [ (* nothing here by default *) ]
     | "power" LEFTA   [ (* nothing here by default *) ]
     | "inv" NONA      [ (* nothing here by default *) ]
-    | "apply" LEFTA
-      [ t1 = term; t2 = term ->
-        let rec aux = function
-          | CicAst.Appl (hd :: tl) -> aux hd @ tl
-          | term -> [term]
-        in
-        CicAst.Appl (aux t1 @ [t2])
-      ]
     | "simple" NONA
       [ sort = sort -> CicAst.Sort sort
       | n = substituted_name -> return_term loc n