X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdoc%2Fprecedence.txt;h=f0a91418d3f64c24a3861a23a14eaa5e68a071d9;hb=a6dd077a2b3e4d0c4395c2ee4cc2e1b6d10ab963;hp=82e8d4ade3c431eada834f3b5ac9e8d4e1f6707a;hpb=5b3048fb48d58e2bd6f726254a06d95a48b2656f;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/doc/precedence.txt b/helm/ocaml/cic_disambiguation/doc/precedence.txt
index 82e8d4ade..f0a91418d 100644
--- a/helm/ocaml/cic_disambiguation/doc/precedence.txt
+++ b/helm/ocaml/cic_disambiguation/doc/precedence.txt
@@ -2,11 +2,15 @@
 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
+\lambda x.x \to x    \lambda. (x \to x)                \to > \lambda
 --------------------------------------------------------------------------------
 
 Precedence total order:
 
-  binder > apply > infix operators
+  \to > lambda > apply > infix operators > binders
+
+where binders are all binders except lambda (i.e. \forall, \pi, \exists)