fixed precedence of \to

[helm.git] / helm / ocaml / cic_disambiguation / cicTextualParser2.ml

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 8e02154ab994c1fcffb0626fdd6e9a93a06f135f..431b15ae83d807617aeef459fbec3d9e621ac068 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -250,8 +250,6 @@ 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
-      | 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 *) ]
@@ -277,6 +275,8 @@ EXTEND
         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