New script dev/tools/change-header to automatically update Coq files headers.

Applied it to fix mli file headers.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13176 85f007b7-540e-0410-9357-904b9bb8a0f7

25 files changed, 175 insertions, 175 deletions

diff --git a/kernel/closure.mli b/kernel/closure.mli
index 9a8ced44e..7becd7c63 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -1,10 +1,10 @@
-(***********************************************************************
-    v      *   The Coq Proof Assistant  /  The Coq Development Team     
-   <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud 
-     \VV/  *************************************************************
-      //   *      This file is distributed under the terms of the       
-           *       GNU Lesser General Public License Version 2.1        
-  ***********************************************************************)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
 
 open Pp
 open Names
diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli
index 0e8201694..1c953d28f 100644
--- a/kernel/conv_oracle.mli
+++ b/kernel/conv_oracle.mli
@@ -1,10 +1,10 @@
-(***********************************************************************
-    v      *   The Coq Proof Assistant  /  The Coq Development Team     
-   <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud 
-     \VV/  *************************************************************
-      //   *      This file is distributed under the terms of the       
-           *       GNU Lesser General Public License Version 2.1        
-  ***********************************************************************)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
 
 open Names
 
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 42991d507..2ca7b17d8 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -1,10 +1,10 @@
-(***********************************************************************
-    v      *   The Coq Proof Assistant  /  The Coq Development Team     
-   <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud 
-     \VV/  *************************************************************
-      //   *      This file is distributed under the terms of the       
-           *       GNU Lesser General Public License Version 2.1        
-  ***********************************************************************)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
 
 open Names
 open Term
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 36af9dc48..de8b081b7 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -1,10 +1,10 @@
-(***********************************************************************
-    v      *   The Coq Proof Assistant  /  The Coq Development Team     
-   <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud 
-     \VV/  *************************************************************
-      //   *      This file is distributed under the terms of the       
-           *       GNU Lesser General Public License Version 2.1        
-  ***********************************************************************)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
 
 open Names
 open Univ
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 78316dd9b..001bc72fe 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -1,10 +1,10 @@
-(***********************************************************************
-    v      *   The Coq Proof Assistant  /  The Coq Development Team     
-   <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud 
-     \VV/  *************************************************************
-      //   *      This file is distributed under the terms of the       
-           *       GNU Lesser General Public License Version 2.1        
-  ***********************************************************************)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
 
 open Names
 open Univ
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 8c31742f3..e1d09e1dc 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -1,10 +1,10 @@
-(***********************************************************************
-    v      *   The Coq Proof Assistant  /  The Coq Development Team     
-   <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud 
-     \VV/  *************************************************************
-      //   *      This file is distributed under the terms of the       
-           *       GNU Lesser General Public License Version 2.1        
-  ***********************************************************************)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
 
 open Names
 open Term
diff --git a/kernel/esubst.mli b/kernel/esubst.mli
index dd7096c4b..73eba7ecd 100644
--- a/kernel/esubst.mli
+++ b/kernel/esubst.mli
@@ -1,10 +1,10 @@
-(***********************************************************************
-    v      *   The Coq Proof Assistant  /  The Coq Development Team     
-   <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud 
-     \VV/  *************************************************************
-      //   *      This file is distributed under the terms of the       
-           *       GNU Lesser General Public License Version 2.1        
-  ***********************************************************************)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
 
 (** Explicit substitutions *)
 
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 40d6912c4..306c407c7 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -1,10 +1,10 @@
-(***********************************************************************
-    v      *   The Coq Proof Assistant  /  The Coq Development Team     
-   <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud 
-     \VV/  *************************************************************
-      //   *      This file is distributed under the terms of the       
-           *       GNU Lesser General Public License Version 2.1        
-  ***********************************************************************)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
 
 open Names
 open Univ
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 42a2da41b..91afda7c3 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -1,10 +1,10 @@
-(***********************************************************************
-    v      *   The Coq Proof Assistant  /  The Coq Development Team     
-   <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud 
-     \VV/  *************************************************************
-      //   *      This file is distributed under the terms of the       
-           *       GNU Lesser General Public License Version 2.1        
-  ***********************************************************************)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
 
 open Names
 open Univ
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index 2514e409c..922ffaf4a 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -1,10 +1,10 @@
-(***********************************************************************
-    v      *   The Coq Proof Assistant  /  The Coq Development Team     
-   <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud 
-     \VV/  *************************************************************
-      //   *      This file is distributed under the terms of the       
-           *       GNU Lesser General Public License Version 2.1        
-  ***********************************************************************)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
 
 (** {6 [Mod_subst] } *)
 
diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli
index 10619820e..3027a6293 100644
--- a/kernel/mod_typing.mli
+++ b/kernel/mod_typing.mli
@@ -1,10 +1,10 @@
-(***********************************************************************
-    v      *   The Coq Proof Assistant  /  The Coq Development Team     
-   <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud 
-     \VV/  *************************************************************
-      //   *      This file is distributed under the terms of the       
-           *       GNU Lesser General Public License Version 2.1        
-  ***********************************************************************)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
 
 open Declarations
 open Environ
diff --git a/kernel/modops.mli b/kernel/modops.mli
index 3ab2961d2..cfa5f9cd9 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -1,10 +1,10 @@
-(***********************************************************************
-    v      *   The Coq Proof Assistant  /  The Coq Development Team     
-   <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud 
-     \VV/  *************************************************************
-      //   *      This file is distributed under the terms of the       
-           *       GNU Lesser General Public License Version 2.1        
-  ***********************************************************************)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
 
 open Util
 open Names
diff --git a/kernel/names.mli b/kernel/names.mli
index 74cebd22a..b441bf00a 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -1,10 +1,10 @@
-(***********************************************************************
-    v      *   The Coq Proof Assistant  /  The Coq Development Team     
-   <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud 
-     \VV/  *************************************************************
-      //   *      This file is distributed under the terms of the       
-           *       GNU Lesser General Public License Version 2.1        
-  ***********************************************************************)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
 
 (** {6 Identifiers } *)
 
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 9078558a9..8c6e69fac 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -1,10 +1,10 @@
-(***********************************************************************
-    v      *   The Coq Proof Assistant  /  The Coq Development Team     
-   <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud 
-     \VV/  *************************************************************
-      //   *      This file is distributed under the terms of the       
-           *       GNU Lesser General Public License Version 2.1        
-  ***********************************************************************)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
 
 open Util
 open Names
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index ced0fd341..dc29d1454 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -1,10 +1,10 @@
-(***********************************************************************
-    v      *   The Coq Proof Assistant  /  The Coq Development Team     
-   <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud 
-     \VV/  *************************************************************
-      //   *      This file is distributed under the terms of the       
-           *       GNU Lesser General Public License Version 2.1        
-  ***********************************************************************)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
 
 open Term
 open Environ
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli
index 0634a99aa..3349a81bc 100644
--- a/kernel/retroknowledge.mli
+++ b/kernel/retroknowledge.mli
@@ -1,10 +1,10 @@
-(***********************************************************************
-    v      *   The Coq Proof Assistant  /  The Coq Development Team     
-   <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud 
-     \VV/  *************************************************************
-      //   *      This file is distributed under the terms of the       
-           *       GNU Lesser General Public License Version 2.1        
-  ***********************************************************************)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
 
 open Names
 open Term
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 3e1051088..a80423272 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -1,10 +1,10 @@
-(***********************************************************************
-    v      *   The Coq Proof Assistant  /  The Coq Development Team     
-   <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud 
-     \VV/  *************************************************************
-      //   *      This file is distributed under the terms of the       
-           *       GNU Lesser General Public License Version 2.1        
-  ***********************************************************************)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
 
 open Names
 open Term
diff --git a/kernel/sign.mli b/kernel/sign.mli
index ddb88287e..4953ff835 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -1,10 +1,10 @@
-(***********************************************************************
-    v      *   The Coq Proof Assistant  /  The Coq Development Team     
-   <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud 
-     \VV/  *************************************************************
-      //   *      This file is distributed under the terms of the       
-           *       GNU Lesser General Public License Version 2.1        
-  ***********************************************************************)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
 
 open Names
 open Term
diff --git a/kernel/subtyping.mli b/kernel/subtyping.mli
index 061a6eb0b..89d532cfd 100644
--- a/kernel/subtyping.mli
+++ b/kernel/subtyping.mli
@@ -1,10 +1,10 @@
-(***********************************************************************
-    v      *   The Coq Proof Assistant  /  The Coq Development Team     
-   <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud 
-     \VV/  *************************************************************
-      //   *      This file is distributed under the terms of the       
-           *       GNU Lesser General Public License Version 2.1        
-  ***********************************************************************)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
 
 open Univ
 open Declarations
diff --git a/kernel/term.mli b/kernel/term.mli
index 5efd95696..12570a434 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -1,10 +1,10 @@
-(***********************************************************************
-    v      *   The Coq Proof Assistant  /  The Coq Development Team     
-   <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud 
-     \VV/  *************************************************************
-      //   *      This file is distributed under the terms of the       
-           *       GNU Lesser General Public License Version 2.1        
-  ***********************************************************************)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
 
 open Names
 
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index dbf479a0c..16adbfb3d 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -1,10 +1,10 @@
-(***********************************************************************
-    v      *   The Coq Proof Assistant  /  The Coq Development Team     
-   <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud 
-     \VV/  *************************************************************
-      //   *      This file is distributed under the terms of the       
-           *       GNU Lesser General Public License Version 2.1        
-  ***********************************************************************)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
 
 open Names
 open Term
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 3a6ad4bb1..5b119159a 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -1,10 +1,10 @@
-(***********************************************************************
-    v      *   The Coq Proof Assistant  /  The Coq Development Team     
-   <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud 
-     \VV/  *************************************************************
-      //   *      This file is distributed under the terms of the       
-           *       GNU Lesser General Public License Version 2.1        
-  ***********************************************************************)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
 
 open Names
 open Term
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index e2df7e983..a6a04aa85 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -1,10 +1,10 @@
-(***********************************************************************
-    v      *   The Coq Proof Assistant  /  The Coq Development Team     
-   <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud 
-     \VV/  *************************************************************
-      //   *      This file is distributed under the terms of the       
-           *       GNU Lesser General Public License Version 2.1        
-  ***********************************************************************)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
 
 open Names
 open Univ
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 1634009b3..3965959d0 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -1,10 +1,10 @@
-(***********************************************************************
-    v      *   The Coq Proof Assistant  /  The Coq Development Team     
-   <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud 
-     \VV/  *************************************************************
-      //   *      This file is distributed under the terms of the       
-           *       GNU Lesser General Public License Version 2.1        
-  ***********************************************************************)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
 
 (** Universes. *)
 
diff --git a/kernel/vconv.mli b/kernel/vconv.mli
index 6776821ed..405ef7a33 100644
--- a/kernel/vconv.mli
+++ b/kernel/vconv.mli
@@ -1,10 +1,10 @@
-(***********************************************************************
-    v      *   The Coq Proof Assistant  /  The Coq Development Team     
-   <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud 
-     \VV/  *************************************************************
-      //   *      This file is distributed under the terms of the       
-           *       GNU Lesser General Public License Version 2.1        
-  ***********************************************************************)
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
 
 open Names
 open Term