THF parser received some care

[helm.git] / helm / software / components / tptp_grafite / astTHF.ml

diff --git a/helm/software/components/tptp_grafite/astTHF.ml b/helm/software/components/tptp_grafite/astTHF.ml
index 541cf98e14ce4ac358585ed3ee3e47e72e690de9..e47c69e650bf52ac61a495bacb57863ebf5c2344 100644 (file)
--- a/helm/software/components/tptp_grafite/astTHF.ml
+++ b/helm/software/components/tptp_grafite/astTHF.ml
@@ -17,6 +17,8 @@ type role =
 
 
 type ast = 
-  | Formula of string * role * CicNotationPt.term
+  | ThfFormula of string * role * CicNotationPt.term
+  | ThfDefinition of string * string * CicNotationPt.term
+  | ThfType of string * string * CicNotationPt.term
   | Comment of string
   | Inclusion of string * (string list)