parameter sintax added to axiom statement

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

diff --git a/helm/software/components/tptp_grafite/parser.mly b/helm/software/components/tptp_grafite/parser.mly
index 05577000cf650f214a101af4f2a8a1d23b1e0d1e..4fe172144a4a2636f11f0d840c42ed07fc9f0624 100644 (file)
--- a/helm/software/components/tptp_grafite/parser.mly
+++ b/helm/software/components/tptp_grafite/parser.mly
@@ -119,6 +119,11 @@
   atomic_word:
     | LNAME { $1 }
     | QSTRING { rm_q $1 }
+    | TYPE { (* workaround! *)
+      match $1 with 
+      | "theorem" -> "theoremP" 
+      | "axiom" -> "axiomP" 
+      | s -> prerr_endline s;assert false }
   ;
   
   formula_source_and_infos: