From: Stefano Zacchiroli Date: Wed, 20 Apr 2005 16:12:01 +0000 (+0000) Subject: changed binding strength of some parsing entries: X-Git-Tag: after_svn_merge~33 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=89c46fa15cd1dd1c9b180e569a27df490c28443d;p=helm.git changed binding strength of some parsing entries: ( a > b means a binds more tightly than b) - now: infix operators > binders > application - previous: application > infix operators > binders --- diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml index d5f427c4f..445871045 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml @@ -225,6 +225,14 @@ EXTEND defs = let_defs; "in"; body = term -> return_term loc (CicAst.LetRec (ind_kind, defs, body)) ] + | "apply" LEFTA + [ t1 = term; t2 = term -> + let rec aux = function + | CicAst.Appl (hd :: tl) -> aux hd @ tl + | term -> [term] + in + CicAst.Appl (aux t1 @ [t2]) + ] | "binder" RIGHTA [ b = binder; @@ -258,14 +266,6 @@ EXTEND | "mult" LEFTA [ (* nothing here by default *) ] | "power" LEFTA [ (* nothing here by default *) ] | "inv" NONA [ (* nothing here by default *) ] - | "apply" LEFTA - [ t1 = term; t2 = term -> - let rec aux = function - | CicAst.Appl (hd :: tl) -> aux hd @ tl - | term -> [term] - in - CicAst.Appl (aux t1 @ [t2]) - ] | "simple" NONA [ sort = sort -> CicAst.Sort sort | n = substituted_name -> return_term loc n