diff --git a/src/core/Heap.ml b/src/core/Heap.ml
index a8f78d08..1e309ab1 100644
--- a/src/core/Heap.ml
+++ b/src/core/Heap.ml
@@ -1,15 +1,3 @@
-(**************************************************************************)
-(*                                                                        *)
-(*                                  Cubicle                               *)
-(*             Combining model checking algorithms and SMT solvers        *)
-(*                                                                        *)
-(*                  Mohamed Iguernelala                                   *)
-(*                  Universite Paris-Sud 11                               *)
-(*                                                                        *)
-(*  Copyright 2011. This file is distributed under the terms of the       *)
-(*  Apache Software License version 2.0                                   *)
-(*                                                                        *)
-(**************************************************************************)
 
 module type RANKED = Heap_intf.RANKED
 
diff --git a/src/core/Heap.mli b/src/core/Heap.mli
index 24c47bd6..a621885c 100644
--- a/src/core/Heap.mli
+++ b/src/core/Heap.mli
@@ -1,16 +1,3 @@
-(**************************************************************************)
-(*                                                                        *)
-(*                                  Cubicle                               *)
-(*             Combining model checking algorithms and SMT solvers        *)
-(*                                                                        *)
-(*                  Mohamed Iguernelala                                   *)
-(*                  Universite Paris-Sud 11                               *)
-(*                                                                        *)
-(*  Copyright 2011. This file is distributed under the terms of the       *)
-(*  Apache Software License version 2.0                                   *)
-(*                                                                        *)
-(**************************************************************************)
-
 module type RANKED = Heap_intf.RANKED
 
 module type S = Heap_intf.S
diff --git a/src/core/Plugin_intf.ml b/src/core/Plugin_intf.ml
index 2584eb52..51a4da72 100644
--- a/src/core/Plugin_intf.ml
+++ b/src/core/Plugin_intf.ml
@@ -1,16 +1,3 @@
-(**************************************************************************)
-(*                                                                        *)
-(*                                  Cubicle                               *)
-(*             Combining model checking algorithms and SMT solvers        *)
-(*                                                                        *)
-(*                  Sylvain Conchon, Evelyne Contejean                    *)
-(*                  Francois Bobot, Mohamed Iguernelala, Alain Mebsout    *)
-(*                  CNRS, Universite Paris-Sud 11                         *)
-(*                                                                        *)
-(*  Copyright 2011. This file is distributed under the terms of the       *)
-(*  Apache Software License version 2.0                                   *)
-(*                                                                        *)
-(**************************************************************************)
 (*
 MSAT is free software, using the Apache license, see file LICENSE
 Copyright 2016 Guillaume Bury
diff --git a/src/core/Solver_types.ml b/src/core/Solver_types.ml
index 5e2686ab..add513cf 100644
--- a/src/core/Solver_types.ml
+++ b/src/core/Solver_types.ml
@@ -1,15 +1,3 @@
-(**************************************************************************)
-(*                                                                        *)
-(*                                  Cubicle                               *)
-(*             Combining model checking algorithms and SMT solvers        *)
-(*                                                                        *)
-(*                  Sylvain Conchon and Alain Mebsout                     *)
-(*                  Universite Paris-Sud 11                               *)
-(*                                                                        *)
-(*  Copyright 2011. This file is distributed under the terms of the       *)
-(*  Apache Software License version 2.0                                   *)
-(*                                                                        *)
-(**************************************************************************)
 (*
 MSAT is free software, using the Apache license, see file LICENSE
 Copyright 2016 Guillaume Bury
diff --git a/src/core/Solver_types.mli b/src/core/Solver_types.mli
index 4d12d93d..62219a3a 100644
--- a/src/core/Solver_types.mli
+++ b/src/core/Solver_types.mli
@@ -1,15 +1,3 @@
-(**************************************************************************)
-(*                                                                        *)
-(*                                  Cubicle                               *)
-(*             Combining model checking algorithms and SMT solvers        *)
-(*                                                                        *)
-(*                  Sylvain Conchon and Alain Mebsout                     *)
-(*                  Universite Paris-Sud 11                               *)
-(*                                                                        *)
-(*  Copyright 2011. This file is distributed under the terms of the       *)
-(*  Apache Software License version 2.0                                   *)
-(*                                                                        *)
-(**************************************************************************)
 (*
 MSAT is free software, using the Apache license, see file LICENSE
 Copyright 2016 Guillaume Bury
diff --git a/src/core/Solver_types_intf.ml b/src/core/Solver_types_intf.ml
index f5076d30..4a1816be 100644
--- a/src/core/Solver_types_intf.ml
+++ b/src/core/Solver_types_intf.ml
@@ -1,15 +1,3 @@
-(**************************************************************************)
-(*                                                                        *)
-(*                                  Cubicle                               *)
-(*             Combining model checking algorithms and SMT solvers        *)
-(*                                                                        *)
-(*                  Sylvain Conchon and Alain Mebsout                     *)
-(*                  Universite Paris-Sud 11                               *)
-(*                                                                        *)
-(*  Copyright 2011. This file is distributed under the terms of the       *)
-(*  Apache Software License version 2.0                                   *)
-(*                                                                        *)
-(**************************************************************************)
 (*
 MSAT is free software, using the Apache license, see file LICENSE
 Copyright 2016 Guillaume Bury
diff --git a/src/core/Theory_intf.ml b/src/core/Theory_intf.ml
index f0183342..7a6621d8 100644
--- a/src/core/Theory_intf.ml
+++ b/src/core/Theory_intf.ml
@@ -1,16 +1,3 @@
-(**************************************************************************)
-(*                                                                        *)
-(*                                  Cubicle                               *)
-(*             Combining model checking algorithms and SMT solvers        *)
-(*                                                                        *)
-(*                  Sylvain Conchon, Evelyne Contejean                    *)
-(*                  Francois Bobot, Mohamed Iguernelala, Alain Mebsout    *)
-(*                  CNRS, Universite Paris-Sud 11                         *)
-(*                                                                        *)
-(*  Copyright 2011. This file is distributed under the terms of the       *)
-(*  Apache Software License version 2.0                                   *)
-(*                                                                        *)
-(**************************************************************************)
 (*
 MSAT is free software, using the Apache license, see file LICENSE
 Copyright 2016 Guillaume Bury