diff --git a/src/core/formula_intf.ml b/src/core/formula_intf.ml
index 08dc9646..61e824dc 100644
--- a/src/core/formula_intf.ml
+++ b/src/core/formula_intf.ml
@@ -39,13 +39,15 @@ module type S = sig
   (** Formula constant. A valid formula should never be physically equal to [dummy] *)
 
   val neg : t -> t
-  (** Formula negation *)
+  (** Formula negation. Should be an involution, i.e. [equal a (neg neg a)] should
+      always hold. *)
 
   val norm : t -> t * negated
   (** Returns a 'normalized' form of the formula, possibly negated
-      (in which case return [Negated]).
-      [norm] must be so that [a] and [neg a] normalise to the same formula,
-      but one returns [Same_sign] and one returns [Negated] *)
+      (in which case return [Negated]). This function is used to recognize
+      the link between a formula [a] and its negation [neg a], so the goal is
+      that [a] and [neg a] normalise to the same formula,
+      but one returns [Same_sign] and the other one returns [Negated] *)
 
 end
 
diff --git a/src/doc.txt b/src/doc.txt
index f3f0f2a2..0b4609cc 100644
--- a/src/doc.txt
+++ b/src/doc.txt
@@ -2,14 +2,18 @@
 
 {2 License}
 
-This code is free, under the Apache 2.0 license.
+This code is free, under the {{:https://github.com/Gbury/mSAT/blob/master/LICENSE}Apache 2.0 license}.
 
 {2 Contents}
 
 mSAT is an ocaml library providing SAT/SMT/McSat solvers. More precisely,
 what mSAT provides are functors to easily create such solvers. Indeed, the core
-of a sat solver does not need much information about neither the exact representation
-of terms nor the inner workings of a theory.
+of a sat solver does not need much information about either the exact representation
+of terms or the inner workings of a theory.
+
+Most modules in mSAT actually define functors. These functors usually take one
+or two arguments, usually an implementation of Terms and formulas used, and an implementation
+of the theory used during solving.
 
 {4 Solver creation}
 
diff --git a/src/solver/solver.mli b/src/solver/solver.mli
index 0b1ae4df..e3400d36 100644
--- a/src/solver/solver.mli
+++ b/src/solver/solver.mli
@@ -17,8 +17,8 @@ module type S = Solver_intf.S
 module DummyTheory(F : Formula_intf.S) :
   Theory_intf.S with type formula = F.t
                  and type proof = F.proof
-(** Simple case where the proof type is the one given in the formula interface
-    and the theory is empty *)
+(** Simple case where the theory is empty and
+    the proof type is the one given in the formula interface *)
 
 module Make (F : Formula_intf.S)
     (Th : Theory_intf.S with type formula = F.t