X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2Fdoc%2Fprecedence.txt;h=09efea85377c901b96b2ef142f59c7723dd6842c;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=f0a91418d3f64c24a3861a23a14eaa5e68a071d9;hpb=0ac46239fb249d740a074a2624c963faa5a70201;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/doc/precedence.txt b/helm/ocaml/cic_disambiguation/doc/precedence.txt
index f0a91418d..09efea853 100644
--- a/helm/ocaml/cic_disambiguation/doc/precedence.txt
+++ b/helm/ocaml/cic_disambiguation/doc/precedence.txt
@@ -2,7 +2,7 @@
 Input                  Should be parsed as             Derived constraint
                                                        on precedence
 --------------------------------------------------------------------------------
-\lambda x.x y          ((\lambda x.x) y)               lambda > 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
@@ -10,7 +10,23 @@ S x = y                  (= (S x) y)                   apply  > infix operators
 
 Precedence total order:
 
-  \to > lambda > apply > infix operators > binders
+  apply > infix operators > to > binders
 
 where binders are all binders except lambda (i.e. \forall, \pi, \exists)
 
+to test:
+  
+./test_parser term << EOT 
+  \lambda x.x y
+  S x = y
+  \forall x.x=x
+  \lambda x.x \to x
+EOT
+  
+should respond with:
+  
+  \lambda x.(x y)
+  (eq (S x) y)
+  \forall x.(eq x x)
+  \lambda x.(x \to x)
+