Porting to MySql.

[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 cd1de44879c723caadc256fd30cbdc8fc72f4e9d..7c0dfc1c6ab31c04a36d7f6ed8189d3cc09fbfa6 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -162,7 +162,7 @@ EXTEND
             return_term loc
               (CicAst.Binder (`Pi, (Cic.Anonymous, Some t1), t2))
       ]
-    | "eq" LEFTA
+    | "relop" LEFTA
       [ t1 = term; SYMBOL "="; t2 = term ->
         return_term loc (CicAst.Appl [CicAst.Symbol ("eq", 0); t1; t2])
       ]
@@ -203,7 +203,9 @@ EXTEND
       | PAREN "("; t = term; PAREN ")" -> return_term loc t
       ]
     ];
-  tactic_where: [ [ where = OPT [ "in"; ident = IDENT -> ident ] -> where ] ];
+  tactic_where: [
+    [ where = OPT [ IDENT "in"; ident = IDENT -> ident ] -> where ]
+  ];
   tactic_term: [ [ t = term -> t ] ];
   ident_list0: [
     [ PAREN "["; idents = LIST0 IDENT SEP SYMBOL ";"; PAREN "]" -> idents ]
@@ -233,7 +235,7 @@ EXTEND
     | IDENT "elim"; IDENT "type"; t = tactic_term ->
         return_tactic loc (TacticAst.ElimType t)
     | IDENT "elim"; t1 = tactic_term;
-      using = OPT [ IDENT "using"; using = tactic_term -> using ] ->
+      using = OPT [ "using"; using = tactic_term -> using ] ->
         return_tactic loc (TacticAst.Elim (t1, using))
     | IDENT "exact"; t = tactic_term -> return_tactic loc (TacticAst.Exact t)
     | IDENT "exists" -> return_tactic loc TacticAst.Exists