From: Enrico Tassi Date: Thu, 19 May 2005 13:19:27 +0000 (+0000) Subject: fix X-Git-Tag: single_binding~32 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=0ac46239fb249d740a074a2624c963faa5a70201;p=helm.git fix --- diff --git a/helm/ocaml/cic_disambiguation/doc/precedence.txt b/helm/ocaml/cic_disambiguation/doc/precedence.txt index f8de4d7a5..f0a91418d 100644 --- a/helm/ocaml/cic_disambiguation/doc/precedence.txt +++ b/helm/ocaml/cic_disambiguation/doc/precedence.txt @@ -5,11 +5,12 @@ Input Should be parsed as Derived constraint \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: - lambda > apply > infix operators > binders + \to > lambda > apply > infix operators > binders where binders are all binders except lambda (i.e. \forall, \pi, \exists)