split precedence level of binders: \lambda has higher precedence than others

[helm.git] / helm / ocaml / cic_disambiguation / doc / precedence.txt

diff --git a/helm/ocaml/cic_disambiguation/doc/precedence.txt b/helm/ocaml/cic_disambiguation/doc/precedence.txt
index 82e8d4ade3c431eada834f3b5ac9e8d4e1f6707a..f8de4d7a56b61a5a50ea37dff1aaba41dedac931 100644 (file)
--- a/helm/ocaml/cic_disambiguation/doc/precedence.txt
+++ b/helm/ocaml/cic_disambiguation/doc/precedence.txt
@@ -2,11 +2,14 @@
 Input                  Should be parsed as             Derived constraint
                                                        on precedence
 --------------------------------------------------------------------------------
-\lambda x.x y          ((\lambda x.x) y)               binder > apply
+\lambda x.x y          ((\lambda x.x) y)               lambda > apply
 S x = y                  (= (S x) y)                   apply  > infix operators
+\forall x.x=x         (\forall x.(= x x))             infix operators > binders
 --------------------------------------------------------------------------------
 
 Precedence total order:
 
-  binder > apply > infix operators
+  lambda > apply > infix operators > binders
+
+where binders are all binders except lambda (i.e. \forall, \pi, \exists)