diff --git a/_tags b/_tags
index 3cb97080..ed5642f1 100644
--- a/_tags
+++ b/_tags
@@ -5,9 +5,10 @@
 <solver/*.cmx>: for-pack(Msat)
 
 # enable stronger inlining everywhere
-<util/{vec,hashcons,hstring,iheap}.cmx>: inline(15)
-<sat/**/*.cmx>: inline(10)
-<smt/**/*.cmx>: inline(10)
+<util/{vec,hashcons,hstring,iheap}.cmx>: inline(100)
+<solver/*.cmx>: inline(1000)
+<sat/**/*.cmx>: inline(100)
+<smt/**/*.cmx>: inline(100)
 
 # more warnings
 <**/*.ml>: warn_K, warn_Y, warn_X
diff --git a/opam b/opam
index bde28dc4..e4e7d2ec 100644
--- a/opam
+++ b/opam
@@ -1,6 +1,6 @@
 opam-version: "1.2"
 license: "Apache"
-version: "1.0"
+version: "1.1"
 author: ["Sylvain Conchon" "Alain Mebsout" "Stephane Lecuyer" "Simon Cruanes" "Guillaume Bury"]
 maintainer: ["guillaume.bury@gmail.com" "simon.cruanes@inria.fr"]
 build: [
diff --git a/solver/solver_types.ml b/solver/solver_types.ml
index 0da5a0f5..af0f4c47 100644
--- a/solver/solver_types.ml
+++ b/solver/solver_types.ml
@@ -15,6 +15,10 @@ open Printf
 
 module type S = Solver_types_intf.S
 
+
+(* Solver types for McSat Solving *)
+(* ************************************************************************ *)
+
 module McMake (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with
     type formula = E.Formula.t and type term = E.Term.t) = struct
 
@@ -308,6 +312,13 @@ module McMake (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with
 
 end
 
+
+
+(* Solver types for pure SAT Solving *)
+(* ************************************************************************ *)
+
+
+
 module SatMake (L : Log_intf.S)(E : Formula_intf.S)
     (Th : Theory_intf.S with type formula = E.t ) = struct