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 d5f427c4f92f039367f722eceb4abf3bb0ce6b68..44587104554a7955fcd0bab31da800b232cf8036 100644 (file)
--- 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