From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 19 May 2009 14:34:01 +0000 (+0000)
Subject: NotEq is now considered as a negative Eq atom
X-Git-Tag: make_still_working~3957
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c43c06062d86bb62bd259537f18aa587699aad9c;p=helm.git

NotEq is now considered as a negative Eq atom
---

diff --git a/helm/software/components/tptp_grafite/tptp2grafite.ml b/helm/software/components/tptp_grafite/tptp2grafite.ml
index 7a714ce07..6b98fe515 100644
--- a/helm/software/components/tptp_grafite/tptp2grafite.ml
+++ b/helm/software/components/tptp_grafite/tptp2grafite.ml
@@ -89,6 +89,7 @@ let rec atom_of_formula neg pos = function
         let neg, pos = atom_of_formula neg pos a in
         atom_of_formula neg pos b 
     | A.NegAtom a -> a::neg, pos 
+    | A.Atom (A.NotEq (a,b)) -> (A.Eq (a,b) :: neg), pos
     | A.Atom a -> neg, a::pos
 ;;