...

diff --git a/helm/software/components/binaries/matitaprover/tptp_cnf.ml b/helm/software/components/binaries/matitaprover/tptp_cnf.ml
index 51ed32431af6eb699cfe11c72d60f6bb2bc292ef..bebce17e7cfeef47d3ed8808d55d6b44ac8c7cf0 100644 (file)
--- 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
 ;;