diff --git a/README.md b/README.md
index 025983e6..93ac820a 100644
--- a/README.md
+++ b/README.md
@@ -1,7 +1,7 @@
 # MSAT  [![Build Status](https://travis-ci.org/Gbury/mSAT.svg?branch=master)](https://travis-ci.org/Gbury/mSAT)
 
 MSAT is an OCaml library that features a modular SAT-solver and some
-extensions (including SMT). This is **work in progress**.
+extensions (including SMT).
 
 
 It derives from [Alt-Ergo Zero](http://cubicle.lri.fr/alt-ergo-zero).
@@ -16,6 +16,21 @@ This program is distributed under the Apache Software License version
 
 See https://gbury.github.io/mSAT/
 
+## INSTALLATION
+
+### Via opam
+
+Once the package is on [opam](http://opam.ocaml.org), just `opam install msat`.
+For the development version, use:
+
+    opam pin add msat https://github.com/Gbury/mSAT.git
+
+### Manual installation
+
+You will need ocamlfind and ocamlbuild. The command is:
+
+    make install
+
 ## USAGE
 
 ### Generic SAT/SMT Solver
@@ -60,20 +75,3 @@ as shown in the following code :
     let _ = Sat.solve ()        (* Should return (Sat.Unsat _) *)
 ```
 
-## INSTALLATION
-
-### Via opam
-
-Once the package is on [opam](http://opam.ocaml.org), just `opam install msat`.
-For the development version, use:
-
-    opam pin add msat https://github.com/Gbury/mSAT.git
-
-### Manual installation
-
-You will need ocamlfind. The command is:
-
-    make install
-
-
-
diff --git a/src/core/plugin_intf.ml b/src/core/plugin_intf.ml
index bfba8585..2c2d703b 100644
--- a/src/core/plugin_intf.ml
+++ b/src/core/plugin_intf.ml
@@ -11,6 +11,11 @@
 (*  Apache Software License version 2.0                                   *)
 (*                                                                        *)
 (**************************************************************************)
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2016 Guillaume Bury
+Copyright 2016 Simon Cruanes
+*)
 
 (** McSat Theory
 
diff --git a/src/core/solver_types.ml b/src/core/solver_types.ml
index 7d4fe172..36fb949b 100644
--- a/src/core/solver_types.ml
+++ b/src/core/solver_types.ml
@@ -10,6 +10,11 @@
 (*  Apache Software License version 2.0                                   *)
 (*                                                                        *)
 (**************************************************************************)
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2016 Guillaume Bury
+Copyright 2016 Simon Cruanes
+*)
 
 open Printf
 
diff --git a/src/core/solver_types.mli b/src/core/solver_types.mli
index 2670096e..b9e76a7a 100644
--- a/src/core/solver_types.mli
+++ b/src/core/solver_types.mli
@@ -10,6 +10,11 @@
 (*  Apache Software License version 2.0                                   *)
 (*                                                                        *)
 (**************************************************************************)
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2016 Guillaume Bury
+Copyright 2016 Simon Cruanes
+*)
 
 (** Internal types (implementation)
 
diff --git a/src/core/solver_types_intf.ml b/src/core/solver_types_intf.ml
index 18ad7fe2..94f23b67 100644
--- a/src/core/solver_types_intf.ml
+++ b/src/core/solver_types_intf.ml
@@ -10,6 +10,11 @@
 (*  Apache Software License version 2.0                                   *)
 (*                                                                        *)
 (**************************************************************************)
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2016 Guillaume Bury
+Copyright 2016 Simon Cruanes
+*)
 
 (** Internal types (interface)
 
diff --git a/src/core/theory_intf.ml b/src/core/theory_intf.ml
index f6e9c263..8df11c20 100644
--- a/src/core/theory_intf.ml
+++ b/src/core/theory_intf.ml
@@ -11,6 +11,11 @@
 (*  Apache Software License version 2.0                                   *)
 (*                                                                        *)
 (**************************************************************************)
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2016 Guillaume Bury
+Copyright 2016 Simon Cruanes
+*)
 
 (** SMT Theory