fixed makefile

[helm.git] / helm / software / components / tptp_grafite / parserTHF.mly

diff --git a/helm/software/components/tptp_grafite/parserTHF.mly b/helm/software/components/tptp_grafite/parserTHF.mly
index 195b79f8de924c1f62ef96892190330de57503fe..99606a956ff0c8014825cba348faa15754f82d82 100644 (file)
--- a/helm/software/components/tptp_grafite/parserTHF.mly
+++ b/helm/software/components/tptp_grafite/parserTHF.mly
@@ -38,7 +38,10 @@ let unreserve k =
   %token IOR
   %token NIEQ
   %token IEQ
+  %token XOR
   %token IMPLY
+  %token IMPLYLR
+  %token COIMPLY
   %token PEQ
   %token DOT
   %token EOF
@@ -148,7 +151,11 @@ let unreserve k =
     | LPAREN term COLON term RPAREN { T.Cast ($2,$4) }
     | term TO term { T.Binder (`Forall,(T.Ident("_",None),Some $1),$3) }
     | term IMPLY term { T.Binder (`Forall,(T.Ident("_",None),Some $1),$3) }
+    | term IMPLYLR term { T.Binder (`Forall,(T.Ident("_",None),Some $3),$1) }
+    | term COIMPLY term { T.Appl [T.Symbol("Iff",0);$1;$3] }
+    | term XOR term { T.Appl [T.Symbol("Xor",0);$1;$3] }
     | term IEQ term { T.Appl [T.Symbol("Eq",0);$1;$3] }
+    | term NIEQ term { T.Appl [T.Symbol("NotEq",0);$1;$3] }
     | term IAND term { T.Appl [T.Symbol("And",0);$1;$3] }
     | term IOR term { T.Appl [T.Symbol("Or",0);$1;$3] }
     | NOT term { T.Appl [T.Symbol("Not",0);$2] }