From d58c5c07566ced7a80638dfd8a54a0162b3b291e Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Wed, 18 Feb 2015 16:32:18 +0100
Subject: [PATCH] Made sat atom type private

---
 _tags       | 2 +-
 msat.mlpack | 3 +++
 msat.odocl  | 2 ++
 sat/sat.ml  | 2 --
 sat/sat.mli | 2 +-
 5 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/_tags b/_tags
index 59ab6e13..491f9fe3 100644
--- a/_tags
+++ b/_tags
@@ -1,4 +1,4 @@
-<util/*.cmx>: package(unix)
+<util/*.cmx>: for-pack(Msat), package(unix)
 <util/*.native>: package(unix)
 <smt/*.cmx>: for-pack(Msat), package(zarith)
 <sat/*.cmx>: for-pack(Msat)
diff --git a/msat.mlpack b/msat.mlpack
index 8dc18c54..1abd2ef0 100644
--- a/msat.mlpack
+++ b/msat.mlpack
@@ -1,3 +1,6 @@
+# Debug
+Log
+
 # Solver Modules
 Log_intf
 Formula_intf
diff --git a/msat.odocl b/msat.odocl
index 573e4c92..72538d43 100644
--- a/msat.odocl
+++ b/msat.odocl
@@ -1,3 +1,5 @@
+util/Log
+
 solver/Log_intf
 solver/Formula_intf
 solver/Expr_intf
diff --git a/sat/sat.ml b/sat/sat.ml
index 9ebb5c17..6ae2b4a6 100644
--- a/sat/sat.ml
+++ b/sat/sat.ml
@@ -7,8 +7,6 @@ Copyright 2014 Simon Cruanes
 module Fsat = struct
   exception Dummy of int
 
-  (* Until the constant true_ and false_ are not needed anymore,
-   * wa can't simply use sigend integers to represent literals *)
   type t = int
 
   let max_lit = max_int
diff --git a/sat/sat.mli b/sat/sat.mli
index af84a079..7de63c20 100644
--- a/sat/sat.mli
+++ b/sat/sat.mli
@@ -4,7 +4,7 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
-module Fsat : Formula_intf.S with type t = int
+module Fsat : Formula_intf.S with type t = private int
 
 module Tseitin : Tseitin.S with type atom = Fsat.t