From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 25 May 2005 13:44:34 +0000 (+0000)
Subject: \lambda x.x y ----> \lambda x.(x y)
X-Git-Tag: single_binding~6
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a4c955f9b69cae88879d366b01ac86fa1ea2b829;p=helm.git

\lambda x.x y ----> \lambda x.(x y)
---

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 431b15ae8..add74d03e 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -250,6 +250,11 @@ EXTEND
         b = binder_low; (vars, typ) = binder_vars; SYMBOL "."; body = term ->
           let binder = mk_binder_ast b typ vars body in
           return_term loc binder
+      | b = binder_high; (vars, typ) = binder_vars; SYMBOL "."; body = term ->
+          let binder = mk_binder_ast b typ vars body in
+          return_term loc binder
+      | t1 = term; SYMBOL <:unicode<to>> (* → *); t2 = term ->
+          return_term loc (CicAst.Binder (`Pi, (Cic.Anonymous, Some t1), t2))
       ]
     | "logic_add" LEFTA   [ (* nothing here by default *) ]
     | "logic_mult" LEFTA  [ (* nothing here by default *) ]
@@ -270,14 +275,6 @@ EXTEND
         in
         CicAst.Appl (aux t1 @ [t2])
       ]
-    | "binder" RIGHTA
-      [
-        b = binder_high; (vars, typ) = binder_vars; SYMBOL "."; body = term ->
-          let binder = mk_binder_ast b typ vars body in
-          return_term loc binder
-      | t1 = term; SYMBOL <:unicode<to>> (* → *); t2 = term ->
-          return_term loc (CicAst.Binder (`Pi, (Cic.Anonymous, Some t1), t2))
-      ]
     | "simple" NONA
       [ sort = sort -> CicAst.Sort sort
       | n = substituted_name -> return_term loc n
diff --git a/helm/ocaml/cic_disambiguation/doc/precedence.txt b/helm/ocaml/cic_disambiguation/doc/precedence.txt
index cd7186fcf..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,7 @@ 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)
 
@@ -25,7 +25,7 @@ EOT
   
 should respond with:
   
-  (\lambda x.x y)
+  \lambda x.(x y)
   (eq (S x) y)
   \forall x.(eq x x)
   \lambda x.(x \to x)