added a lot of notation: arithmetic operators, relational operators, ...

[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 efe959de8cace2f434db20f3a48ad82783770e64..26fc36c78795966aae33cb0613c212862fecf8b9 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])
       ]