From d6c87f235a98c05a26b4a0e87129335d034219af Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 22 Jun 2010 06:31:30 +0000
Subject: 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
---
 interp/constrextern.mli         | 14 +++++++-------
 interp/constrintern.mli         | 14 +++++++-------
 interp/coqlib.mli               | 14 +++++++-------
 interp/dumpglob.mli             | 14 +++++++-------
 interp/genarg.mli               | 14 +++++++-------
 interp/implicit_quantifiers.mli | 14 +++++++-------
 interp/modintern.mli            | 14 +++++++-------
 interp/notation.mli             | 14 +++++++-------
 interp/ppextend.mli             | 14 +++++++-------
 interp/reserve.mli              | 14 +++++++-------
 interp/smartlocate.mli          | 14 +++++++-------
 interp/syntax_def.mli           | 14 +++++++-------
 interp/topconstr.mli            | 14 +++++++-------
 13 files changed, 91 insertions(+), 91 deletions(-)

(limited to 'interp')

diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index ac3a388332..7bc2ddcecc 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.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/interp/constrintern.mli b/interp/constrintern.mli
index 880f8a4be2..62821081f5 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.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/interp/coqlib.mli b/interp/coqlib.mli
index 1d7f571b3a..73427d902d 100644
--- a/interp/coqlib.mli
+++ b/interp/coqlib.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/interp/dumpglob.mli b/interp/dumpglob.mli
index 7efa6f1e01..0236084909 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.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        *)
+(************************************************************************)
 
 val open_glob_file : string -> unit
 val close_glob_file : unit -> unit
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 984f479fb7..0ab3b43202 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.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/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 0b2ac3e71c..cf3989f890 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.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/interp/modintern.mli b/interp/modintern.mli
index 5dacfd0700..c5940bfffe 100644
--- a/interp/modintern.mli
+++ b/interp/modintern.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/interp/notation.mli b/interp/notation.mli
index 3da9ec0e5a..17d8ad8f25 100644
--- a/interp/notation.mli
+++ b/interp/notation.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/interp/ppextend.mli b/interp/ppextend.mli
index 19ca913e88..99152c0456 100644
--- a/interp/ppextend.mli
+++ b/interp/ppextend.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/interp/reserve.mli b/interp/reserve.mli
index e53ad8365a..184eb21836 100644
--- a/interp/reserve.mli
+++ b/interp/reserve.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/interp/smartlocate.mli b/interp/smartlocate.mli
index 0cd261a82e..b5a89949f7 100644
--- a/interp/smartlocate.mli
+++ b/interp/smartlocate.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/interp/syntax_def.mli b/interp/syntax_def.mli
index 0190676084..94252950b6 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.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/interp/topconstr.mli b/interp/topconstr.mli
index b288fe8b5c..3a50475dbe 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.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
-- 
cgit v1.2.3