diff --git a/examples/use_api/transform.ml b/examples/use_api/transform.ml
index 62e5cc22830d3d2e9fc648b830bc8e6827278b61..02fb3b38d45eea982cf7908901398c841e584408 100644
--- a/examples/use_api/transform.ml
+++ b/examples/use_api/transform.ml
@@ -1,3 +1,13 @@
+(********************************************************************)
+(*                                                                  *)
+(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
+(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
+(*                                                                  *)
+(*  This software is distributed under the terms of the GNU Lesser  *)
+(*  General Public License version 2.1, with the special exception  *)
+(*  on linking described in file LICENSE.                           *)
+(*                                                                  *)
+(********************************************************************)
 
 
 open Why3
diff --git a/misc/headache_config.txt b/misc/headache_config.txt
index 01cba08865f20c26e5dc8175b363bfcff31cc14d..885ec8e9c3713d40e16659d30c373aeeff8d11a7 100644
--- a/misc/headache_config.txt
+++ b/misc/headache_config.txt
@@ -2,6 +2,7 @@
 | "META.in" -> no
 | "extmap.ml[i]?" -> no
 | "literals.mll" -> no
+| "report.ml[i]?" -> no
 # Objective Caml source
 | ".*\\.ml[il4]?" -> frame width:62 open:"(*" line:"*" close:"*)"
 | ".*\\.ml[il4]?\\.in" -> frame width:62 open:"(*" line:"*" close:"*)"
diff --git a/src/jessie/literals.mll b/src/jessie/literals.mll
index c6381410c6c6a017211b6e8a3bb8c8cdcec56fe0..bd70e9053112049bf55e8fc2de4105dc6f998860 100644
--- a/src/jessie/literals.mll
+++ b/src/jessie/literals.mll
@@ -3,7 +3,7 @@
 (*  This file is part of Frama-C.                                         *)
 (*                                                                        *)
 (*  Copyright (C) 2007-2012                                               *)
-(*    CEA   (Commissariat � l'�nergie atomique et aux �nergies            *)
+(*    CEA   (Commissariat à l'énergie atomique et aux énergies            *)
 (*           alternatives)                                                *)
 (*    INRIA (Institut National de Recherche en Informatique et en         *)
 (*           Automatique)                                                 *)
diff --git a/src/mlw/cakeml_printer.ml b/src/mlw/cakeml_printer.ml
index 50d617f79ad3e43743555a8a6e3d65b2e5802b21..b5d83079ffcc140d6a63caf762814060d8fa4abe 100644
--- a/src/mlw/cakeml_printer.ml
+++ b/src/mlw/cakeml_printer.ml
@@ -8,6 +8,7 @@
 (*  on linking described in file LICENSE.                           *)
 (*                                                                  *)
 (********************************************************************)
+
 open Compile
 open Format
 open Ident
diff --git a/src/mlw/ml_printer.mli b/src/mlw/ml_printer.mli
index 5359b291a31de6f36a64acdb971c275b265c289d..b80838e6eb279024a9349430f09931c4683d46b2 100644
--- a/src/mlw/ml_printer.mli
+++ b/src/mlw/ml_printer.mli
@@ -1,3 +1,14 @@
+(********************************************************************)
+(*                                                                  *)
+(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
+(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
+(*                                                                  *)
+(*  This software is distributed under the terms of the GNU Lesser  *)
+(*  General Public License version 2.1, with the special exception  *)
+(*  on linking described in file LICENSE.                           *)
+(*                                                                  *)
+(********************************************************************)
+
 open Pp
 open Printer
 open Mltree
diff --git a/src/mlw/mlinterp.ml b/src/mlw/mlinterp.ml
index 7322593ea3b6a6b7e172cb4493d59641d96c9d2c..1d6df16bc40269f0450cf2d269b994ce31394c2a 100644
--- a/src/mlw/mlinterp.ml
+++ b/src/mlw/mlinterp.ml
@@ -1,3 +1,14 @@
+(********************************************************************)
+(*                                                                  *)
+(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
+(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
+(*                                                                  *)
+(*  This software is distributed under the terms of the GNU Lesser  *)
+(*  General Public License version 2.1, with the special exception  *)
+(*  on linking described in file LICENSE.                           *)
+(*                                                                  *)
+(********************************************************************)
+
 open Term
 open Ty
 open Decl
diff --git a/src/mlw/mlinterp.mli b/src/mlw/mlinterp.mli
index 4bb8b26949d4e3a028af1fc812f28739ed90ad6d..73fc03244d320718511e97247d610f3654654a90 100644
--- a/src/mlw/mlinterp.mli
+++ b/src/mlw/mlinterp.mli
@@ -1,3 +1,14 @@
+(********************************************************************)
+(*                                                                  *)
+(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
+(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
+(*                                                                  *)
+(*  This software is distributed under the terms of the GNU Lesser  *)
+(*  General Public License version 2.1, with the special exception  *)
+(*  on linking described in file LICENSE.                           *)
+(*                                                                  *)
+(********************************************************************)
+
 open Wstdlib
 
 type value =
diff --git a/src/transform/abstract_quantifiers.ml b/src/transform/abstract_quantifiers.ml
index 7530b3cf65a314a09e64c9812d5de0bade1b1310..4ae305ad3b03ce23ca0ab157013e4d6041a433ee 100644
--- a/src/transform/abstract_quantifiers.ml
+++ b/src/transform/abstract_quantifiers.ml
@@ -1,3 +1,14 @@
+(********************************************************************)
+(*                                                                  *)
+(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
+(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
+(*                                                                  *)
+(*  This software is distributed under the terms of the GNU Lesser  *)
+(*  General Public License version 2.1, with the special exception  *)
+(*  on linking described in file LICENSE.                           *)
+(*                                                                  *)
+(********************************************************************)
+
 open Term
 open Decl
 
diff --git a/src/transform/eliminate_symbol.ml b/src/transform/eliminate_symbol.ml
index 68e6385eacdca178c190d8a60c58ae5e6381c8e0..17fad1913dcf840716f0ee07f586e8b4f6b49b77 100644
--- a/src/transform/eliminate_symbol.ml
+++ b/src/transform/eliminate_symbol.ml
@@ -1,7 +1,7 @@
 (********************************************************************)
 (*                                                                  *)
 (*  The Why3 Verification Platform   /   The Why3 Development Team  *)
-(*  Copyright 2010-2016   --   INRIA - CNRS - Paris-Sud University  *)
+(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
 (*                                                                  *)
 (*  This software is distributed under the terms of the GNU Lesser  *)
 (*  General Public License version 2.1, with the special exception  *)
diff --git a/src/transform/eliminate_unknown_lsymbols.ml b/src/transform/eliminate_unknown_lsymbols.ml
index 0ebaa5232dd622913cc04224ee099d52c7e124c4..9a7007beef35a01d440950a24ebc3958acfe81cc 100644
--- a/src/transform/eliminate_unknown_lsymbols.ml
+++ b/src/transform/eliminate_unknown_lsymbols.ml
@@ -1,3 +1,14 @@
+(********************************************************************)
+(*                                                                  *)
+(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
+(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
+(*                                                                  *)
+(*  This software is distributed under the terms of the GNU Lesser  *)
+(*  General Public License version 2.1, with the special exception  *)
+(*  on linking described in file LICENSE.                           *)
+(*                                                                  *)
+(********************************************************************)
+
 open Term
 open Decl
 open Theory
diff --git a/src/transform/eliminate_unknown_types.ml b/src/transform/eliminate_unknown_types.ml
index 9ec9f4ba3038214f9c9515c64bb3b8d87b050098..54973720675583a9582cb18c7c25b7d14eaee930 100644
--- a/src/transform/eliminate_unknown_types.ml
+++ b/src/transform/eliminate_unknown_types.ml
@@ -1,3 +1,14 @@
+(********************************************************************)
+(*                                                                  *)
+(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
+(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
+(*                                                                  *)
+(*  This software is distributed under the terms of the GNU Lesser  *)
+(*  General Public License version 2.1, with the special exception  *)
+(*  on linking described in file LICENSE.                           *)
+(*                                                                  *)
+(********************************************************************)
+
 open Term
 open Decl
 open Theory
diff --git a/src/transform/matching.ml b/src/transform/matching.ml
index 74c49048fcf1c79689c24d69c7a017d1c0d64d82..1b565de9c28691fec872fd7505664123f4052532 100644
--- a/src/transform/matching.ml
+++ b/src/transform/matching.ml
@@ -1,3 +1,13 @@
+(********************************************************************)
+(*                                                                  *)
+(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
+(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
+(*                                                                  *)
+(*  This software is distributed under the terms of the GNU Lesser  *)
+(*  General Public License version 2.1, with the special exception  *)
+(*  on linking described in file LICENSE.                           *)
+(*                                                                  *)
+(********************************************************************)
 
 open Ident
 open Ty
diff --git a/src/transform/reflection.ml b/src/transform/reflection.ml
index 0ddaecccf69f82e27ac2830b9f8748d53e3cb171..c6cfdcbb7659c4b26ea219cf14c4986577019169 100644
--- a/src/transform/reflection.ml
+++ b/src/transform/reflection.ml
@@ -1,3 +1,14 @@
+(********************************************************************)
+(*                                                                  *)
+(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
+(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
+(*                                                                  *)
+(*  This software is distributed under the terms of the GNU Lesser  *)
+(*  General Public License version 2.1, with the special exception  *)
+(*  on linking described in file LICENSE.                           *)
+(*                                                                  *)
+(********************************************************************)
+
 open Term
 open Ty
 open Decl
diff --git a/src/transform/reflection.mli b/src/transform/reflection.mli
index 52ec3921904e3bd1323a114dede0ac55cc771a6c..e7a8c2d7e66a8e97da9de9d2b6974173b8efe54b 100644
--- a/src/transform/reflection.mli
+++ b/src/transform/reflection.mli
@@ -1,3 +1,14 @@
+(********************************************************************)
+(*                                                                  *)
+(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
+(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
+(*                                                                  *)
+(*  This software is distributed under the terms of the GNU Lesser  *)
+(*  General Public License version 2.1, with the special exception  *)
+(*  on linking described in file LICENSE.                           *)
+(*                                                                  *)
+(********************************************************************)
+
 val reflection_by_lemma: Decl.prsymbol -> Env.env -> Task.task Trans.tlist
 
 val reflection_by_function: bool -> string -> Env.env -> Task.task Trans.tlist
diff --git a/src/util/debug_optim.ml b/src/util/debug_optim.ml
index 1d5e22a0f63e94b9c57f959a0dc72a2a40f172df..585f0773236ed117e7de76d3f32d4f906a1dd5c1 100644
--- a/src/util/debug_optim.ml
+++ b/src/util/debug_optim.ml
@@ -1,3 +1,14 @@
+(********************************************************************)
+(*                                                                  *)
+(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
+(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
+(*                                                                  *)
+(*  This software is distributed under the terms of the GNU Lesser  *)
+(*  General Public License version 2.1, with the special exception  *)
+(*  on linking described in file LICENSE.                           *)
+(*                                                                  *)
+(********************************************************************)
+
 open Parsetree
 open Ast_mapper
 open Asttypes