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

27 files changed, 189 insertions, 190 deletions

diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index cc064bc4da..1d8df523fc 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.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/pretyping/cbv.mli b/pretyping/cbv.mli
index 50b4fda4a3..5c0ff6027d 100644
--- a/pretyping/cbv.mli
+++ b/pretyping/cbv.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/pretyping/classops.mli b/pretyping/classops.mli
index 6184ed7a1e..ba6eb4ca67 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.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 Decl_kinds
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index a5ed740f96..7da8851f64 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.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 Evd
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 47a7beb539..ebca020ab3 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.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/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 1ddf97c861..578318a83d 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.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 Sign
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index e21516681b..1d11097d30 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.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/pretyping/evd.mli b/pretyping/evd.mli
index 87e703463f..24d865beb7 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -1,11 +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/pretyping/indrec.mli b/pretyping/indrec.mli
index 7f19c5d372..511ec9c51e 100644
--- a/pretyping/indrec.mli
+++ b/pretyping/indrec.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/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 98a22fabd4..7c5642d1de 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.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/pretyping/matching.mli b/pretyping/matching.mli
index eb9c8fc8c6..86657d2879 100644
--- a/pretyping/matching.mli
+++ b/pretyping/matching.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        *)
+(************************************************************************)
 
 (** This module implements pattern-matching on terms *)
 
diff --git a/pretyping/namegen.mli b/pretyping/namegen.mli
index 889f8ec8cd..5560cddf75 100644
--- a/pretyping/namegen.mli
+++ b/pretyping/namegen.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/pretyping/pattern.mli b/pretyping/pattern.mli
index 3b61c1e437..5685f3d2c5 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.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        *)
+(************************************************************************)
 
 (** This module defines the type of pattern used for pattern-matching
     terms in tatics *)
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index f55e70befc..0bdbb1c65b 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_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 Pp
 open Util
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 00eb613abc..d6996dd3b7 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.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        *)
+(************************************************************************)
 
 (** This file implements type inference. It maps [rawconstr]
    (i.e. untyped terms whose names are located) to [constr]. In
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 0c8f154726..d7f8311c79 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.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        *)
+(************************************************************************)
 
 (**Untyped intermediate terms, after constr_expr and before constr
 
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 5651b7687f..6ad5fbc643 100755..100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.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 Nametab
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 4518c693de..40c0e28139 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.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/pretyping/retyping.mli b/pretyping/retyping.mli
index 5b445ff9c0..2733b1473f 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.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/pretyping/tacred.mli b/pretyping/tacred.mli
index fdceadfbb3..4793027fba 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.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/pretyping/term_dnet.mli b/pretyping/term_dnet.mli
index 3db55b1621..242fc8cd7b 100644
--- a/pretyping/term_dnet.mli
+++ b/pretyping/term_dnet.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 Sign
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index 050084bb17..fc227b5fb2 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.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 Pp
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index dc1c5f5569..ebdfe25c41 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.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 Libnames
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index 43b3495150..8f21510b0b 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_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 Decl_kinds
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index 90f823b8e1..9bfc26057b 100644
--- a/pretyping/typing.mli
+++ b/pretyping/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 Term
 open Environ
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 8829d8989d..8cd7003edc 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.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/pretyping/vnorm.mli b/pretyping/vnorm.mli
index da9e7cf1e5..2820b1b4f6 100644
--- a/pretyping/vnorm.mli
+++ b/pretyping/vnorm.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