diff --git a/src/backend/dedukti.mli b/src/backend/dedukti.mli
index be352eb3..449b82fb 100644
--- a/src/backend/dedukti.mli
+++ b/src/backend/dedukti.mli
@@ -1,3 +1,13 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2014 Guillaume Bury
+Copyright 2014 Simon Cruanes
+*)
+
+(** Deduki backend for proofs
+
+    Work in progress...
+*)
 
 module type S = Backend_intf.S
 
diff --git a/src/core/external.mli b/src/core/external.mli
index 7edc9f9c..7a2c9ed8 100644
--- a/src/core/external.mli
+++ b/src/core/external.mli
@@ -4,7 +4,14 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
+(** mSAT safe interface
+
+    This module defines a safe interface for the core solver.
+    It is the basis of the {!module:Solver} and {!module:Mcsolver} modules.
+*)
+
 module type S = Solver_intf.S
+(** Safe external interface of solvers. *)
 
 module Make
     (St : Solver_types.S)
@@ -13,5 +20,6 @@ module Make
                          and type proof = St.proof)
     (Dummy : sig end) :
   S with module St = St
+(** Functor to make a safe external interface. *)
 
 
diff --git a/src/core/internal.mli b/src/core/internal.mli
index 0ac8fa72..c00b5d29 100644
--- a/src/core/internal.mli
+++ b/src/core/internal.mli
@@ -4,6 +4,14 @@ Copyright 2014 Guillaume Bury
 Copyright 2014 Simon Cruanes
 *)
 
+(** mSAT core
+
+    This is the core of msat, containing the code doing the actual solving.
+    This module is based on mini-sat, and as such the solver heavily uses mutation,
+    which makes using it direclty kinda tricky (some exceptions can be raised
+    at surprising times, mutating is dangerous for maintaining invariants, etc...).
+*)
+
 module Make
   (St : Solver_types.S)
   (Th : Plugin_intf.S with type term = St.term and type formula = St.formula and type proof = St.proof)
diff --git a/src/core/solver_intf.ml b/src/core/solver_intf.ml
index c79d4457..b4673374 100644
--- a/src/core/solver_intf.ml
+++ b/src/core/solver_intf.ml
@@ -5,9 +5,11 @@ Copyright 2016 Simon Cruanes
 *)
 
 (** Interface for Solvers
+
     This modules defines the safe external interface for solvers.
     Solvers that implements this interface can be obtained using the [Make]
-    functor in {!Solver} or {!Mcsolver}. *)
+    functor in {!Solver} or {!Mcsolver}.
+*)
 
 type ('term, 'form) sat_state = {
   eval: 'form -> bool;
@@ -57,8 +59,8 @@ module type S = sig
   (** The type of atoms given by the module argument for formulas *)
 
   type res =
-    | Sat of (St.term,St.formula) sat_state
-    | Unsat of (St.clause,Proof.proof) unsat_state (**)
+    | Sat of (St.term,St.formula) sat_state         (** Returned when the solver reaches SAT *)
+    | Unsat of (St.clause,Proof.proof) unsat_state  (** Returned when the solver reaches UNSAT *)
   (** Result type for the solver *)
 
   exception UndecidedLit
diff --git a/src/core/solver_types.mli b/src/core/solver_types.mli
index f4b0353a..2670096e 100644
--- a/src/core/solver_types.mli
+++ b/src/core/solver_types.mli
@@ -11,7 +11,17 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(** Internal types (implementation)
+
+    This modules actually implements the internal types used by the solver.
+    Since mutation is heavily used in the solver, it is really, really, *really*
+    discouraged to direclty use the functions in this module if you don't know the
+    inner working of mSAT perfectly as even the simplest
+    change can have dramatic effects on the solver.
+*)
+
 module type S = Solver_types_intf.S
+(** Interface for the internal types. *)
 
 module McMake (E : Expr_intf.S)(Dummy : sig end):
     S with type term = E.Term.t and type formula = E.Formula.t and type proof = E.proof
diff --git a/src/core/solver_types_intf.ml b/src/core/solver_types_intf.ml
index d2cbd691..18ad7fe2 100644
--- a/src/core/solver_types_intf.ml
+++ b/src/core/solver_types_intf.ml
@@ -11,10 +11,17 @@
 (*                                                                        *)
 (**************************************************************************)
 
+(** Internal types (interface)
+
+    This modules defines the interface of most of the internal types
+    used in the core solver.
+*)
+
 module type S = sig
   (** The signatures of clauses used in the Solver. *)
 
   val mcsat : bool
+  (** TODO:deprecate. *)
 
   (** {2 Type definitions} *)
 
diff --git a/src/solver/mcsolver.mli b/src/solver/mcsolver.mli
index 53e81531..455eb92e 100644
--- a/src/solver/mcsolver.mli
+++ b/src/solver/mcsolver.mli
@@ -5,7 +5,9 @@ Copyright 2014 Simon Cruanes
 *)
 
 (** Create McSat solver
-    This module provides a functor to create an McSAt solver. *)
+
+    This module provides a functor to create an McSAt solver.
+*)
 
 module type S = Solver_intf.S
 (** The interface exposed by the solver. *)
diff --git a/src/solver/solver.mli b/src/solver/solver.mli
index 15e49b10..1fbb30b0 100644
--- a/src/solver/solver.mli
+++ b/src/solver/solver.mli
@@ -5,9 +5,11 @@ Copyright 2014 Simon Cruanes
 *)
 
 (** Create SAT/SMT Solvers
+
     This module provides a functor to create an SMT solver. Additionally, it also
     gives a functor that produce an adequate empty theory that can be given to the [Make]
-    functor in order to create a pure SAT solver. *)
+    functor in order to create a pure SAT solver.
+*)
 
 module type S = Solver_intf.S
 (** The interface of instantiated solvers. *)