From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 25 Jun 2009 14:45:37 +0000 (+0000)
Subject: ...
X-Git-Tag: make_still_working~3797
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a198c6eb150b16ca6f16e2ae75f948a3e75cab2e;p=helm.git

...
---

diff --git a/helm/software/components/binaries/matitaprover/tptp_cnf.ml b/helm/software/components/binaries/matitaprover/tptp_cnf.ml
index 51ed32431..bebce17e7 100644
--- a/helm/software/components/binaries/matitaprover/tptp_cnf.ml
+++ b/helm/software/components/binaries/matitaprover/tptp_cnf.ml
@@ -2,8 +2,8 @@
 let trans_atom ~neg = function 
   | Ast.True | Ast.False | Ast.Predicate _ | Ast.Proposition _ -> assert false
   | Ast.Eq _ when neg -> assert false
-  | Ast.Eq (a,b) -> Ast.Function ("==",[Ast.Constant "Ω"; a; b])
-  | Ast.NotEq (a,b) when neg -> Ast.Function ("==",[Ast.Constant "Ω"; a; b])
+  | Ast.Eq (a,b) -> Ast.Function ("==",[Ast.Constant "_"; a; b])
+  | Ast.NotEq (a,b) when neg -> Ast.Function ("==",[Ast.Constant "_"; a; b])
   | Ast.NotEq _ -> assert false
 ;;