From 763cf4f37e10d9a0e8a2a0e9286c02708a60bf08 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 16 Jul 2004 20:01:26 +0000
Subject: Nouvelle en-tête

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/closure.ml       | 18 +++++++++---------
 kernel/closure.mli      | 22 +++++++++++-----------
 kernel/conv_oracle.ml   | 14 +++++++-------
 kernel/conv_oracle.mli  | 14 +++++++-------
 kernel/cooking.ml       | 14 +++++++-------
 kernel/cooking.mli      | 14 +++++++-------
 kernel/declarations.ml  | 14 +++++++-------
 kernel/declarations.mli | 14 +++++++-------
 kernel/entries.ml       | 14 +++++++-------
 kernel/entries.mli      | 14 +++++++-------
 kernel/environ.ml       | 14 +++++++-------
 kernel/environ.mli      | 30 +++++++++++++++---------------
 kernel/esubst.ml        | 14 +++++++-------
 kernel/esubst.mli       | 14 +++++++-------
 kernel/indtypes.ml      | 32 ++++++++++++++++----------------
 kernel/indtypes.mli     | 14 +++++++-------
 kernel/inductive.ml     | 38 +++++++++++++++++++-------------------
 kernel/inductive.mli    | 14 +++++++-------
 kernel/mod_typing.ml    | 14 +++++++-------
 kernel/mod_typing.mli   | 14 +++++++-------
 kernel/modops.ml        | 14 +++++++-------
 kernel/modops.mli       | 14 +++++++-------
 kernel/names.ml         | 14 +++++++-------
 kernel/names.mli        | 14 +++++++-------
 kernel/reduction.ml     | 14 +++++++-------
 kernel/reduction.mli    | 22 +++++++++++-----------
 kernel/safe_typing.ml   | 14 +++++++-------
 kernel/safe_typing.mli  | 14 +++++++-------
 kernel/sign.ml          | 14 +++++++-------
 kernel/sign.mli         | 14 +++++++-------
 kernel/subtyping.ml     | 14 +++++++-------
 kernel/subtyping.mli    | 14 +++++++-------
 kernel/term.ml          | 18 +++++++++---------
 kernel/term.mli         | 14 +++++++-------
 kernel/term_typing.ml   | 14 +++++++-------
 kernel/term_typing.mli  | 14 +++++++-------
 kernel/type_errors.ml   | 14 +++++++-------
 kernel/type_errors.mli  | 14 +++++++-------
 kernel/typeops.ml       | 18 +++++++++---------
 kernel/typeops.mli      | 14 +++++++-------
 kernel/univ.ml          | 14 +++++++-------
 kernel/univ.mli         | 14 +++++++-------
 42 files changed, 337 insertions(+), 337 deletions(-)

(limited to 'kernel')

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 1d85089e9d..f4db948a02 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -1,10 +1,10 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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        *)
+(************************************************************************)
 
 (* $Id$ *)
 
@@ -1006,7 +1006,7 @@ and knht e t stk =
         (mk_clos2 e t, stk)
 
 
-(***********************************************************************)
+(************************************************************************)
 
 (* Computes a normal form from the result of knh. *)
 let rec knr info m stk =
@@ -1059,7 +1059,7 @@ and knit info e t stk =
 
 let kh info v stk = fapp_stack(kni info v stk)
 
-(***********************************************************************)
+(************************************************************************)
 
 let rec zip_term zfun m stk =
   match stk with
diff --git a/kernel/closure.mli b/kernel/closure.mli
index e045bd60fc..e0cfe7b51a 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -1,10 +1,10 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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        *)
+(************************************************************************)
 
 (*i $Id$ i*)
 
@@ -82,7 +82,7 @@ val betadeltaiotanolet : reds
 
 val unfold_red : evaluable_global_reference -> reds
 
-(***********************************************************************)
+(************************************************************************)
 
 type table_key =
   | ConstKey of constant
@@ -95,7 +95,7 @@ val ref_value_cache: 'a infos -> table_key -> 'a option
 val info_flags: 'a infos -> reds
 val create: ('a infos -> constr -> 'a) -> reds -> env -> 'a infos
 
-(***********************************************************************)
+(************************************************************************)
 (*s A [stack] is a context of arguments, arguments are pushed by
    [append_stack] one array at a time but popped with [decomp_stack]
    one by one *)
@@ -121,7 +121,7 @@ val app_stack : constr * constr stack -> constr
 val stack_tail : int -> 'a stack -> 'a stack
 val stack_nth : 'a stack -> int -> 'a
 
-(***********************************************************************)
+(************************************************************************)
 (*s Lazy reduction. *)
 
 (* [fconstr] is the type of frozen constr *)
@@ -185,7 +185,7 @@ val unfold_reference : clos_infos -> table_key -> fconstr option
 (* [mind_equiv] checks whether two mutual inductives are intentionally equal *)
 val mind_equiv : clos_infos -> mutual_inductive -> mutual_inductive -> bool
 
-(***********************************************************************)
+(************************************************************************)
 (*i This is for lazy debug *)
 
 val lift_fconstr      : int -> fconstr -> fconstr
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index 527030fb4c..11d4435c2f 100644
--- a/kernel/conv_oracle.ml
+++ b/kernel/conv_oracle.ml
@@ -1,10 +1,10 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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        *)
+(************************************************************************)
 
 (* $Id$ *)
 
diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli
index 0eefb87112..8dad2e2bdb 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___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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        *)
+(************************************************************************)
 
 (* $Id$ *)
 
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 7c3b8e60f0..c37c81cf60 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -1,10 +1,10 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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        *)
+(************************************************************************)
 
 (*i $Id$ i*)
 
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index b54189ba64..7bd64d3267 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -1,10 +1,10 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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        *)
+(************************************************************************)
 
 (*i $Id$ i*)
 
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 0aa5c99489..152c1e5bf8 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -1,10 +1,10 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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        *)
+(************************************************************************)
 
 (*i $Id$ i*)
 
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 7c6d3ecdf3..a168abdfb2 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -1,10 +1,10 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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        *)
+(************************************************************************)
 
 (*i $Id$ i*)
 
diff --git a/kernel/entries.ml b/kernel/entries.ml
index e383dbabd7..4d485ff8cc 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -1,10 +1,10 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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        *)
+(************************************************************************)
 
 (*i $Id$ i*)
 
diff --git a/kernel/entries.mli b/kernel/entries.mli
index e383dbabd7..4d485ff8cc 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -1,10 +1,10 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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        *)
+(************************************************************************)
 
 (*i $Id$ i*)
 
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 9d81e8f001..41b664309d 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -1,10 +1,10 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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        *)
+(************************************************************************)
 
 (* $Id$ *)
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 540fd02d3d..71fc8e6d8a 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -1,10 +1,10 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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        *)
+(************************************************************************)
 
 (*i $Id$ i*)
 
@@ -43,7 +43,7 @@ val engagement    : env -> engagement option
 (* is the local context empty *)
 val empty_context : env -> bool
 
-(***********************************************************************)
+(************************************************************************)
 (*s Context of de Bruijn variables (rel_context) *)
 val push_rel         : rel_declaration -> env -> env
 val push_rel_context :     rel_context -> env -> env
@@ -58,7 +58,7 @@ val evaluable_rel : int -> env -> bool
 val fold_rel_context :
   (env -> rel_declaration -> 'a -> 'a) -> env -> init:'a -> 'a
 
-(***********************************************************************)
+(************************************************************************)
 (* Context of variables (section variables and goal assumptions) *)
 val push_named : named_declaration -> env -> env
 
@@ -80,7 +80,7 @@ val reset_context : env -> env
 (* This forgets rel context and sets a new named context *)
 val reset_with_named_context : named_context -> env -> env
 
-(***********************************************************************)
+(************************************************************************)
 (*s Global constants *)
 (*s Add entries to global environment *)
 val add_constant : constant -> constant_body -> env -> env
@@ -100,7 +100,7 @@ val constant_value     : env -> constant -> constr
 val constant_type      : env -> constant -> types
 val constant_opt_value : env -> constant -> constr option
 
-(***********************************************************************)
+(************************************************************************)
 (*s Inductive types *)
 val add_mind : mutual_inductive -> mutual_inductive_body -> env -> env
 
@@ -108,7 +108,7 @@ val add_mind : mutual_inductive -> mutual_inductive_body -> env -> env
 (* raises [Not_found] if the required path is not found *)
 val lookup_mind : mutual_inductive -> env -> mutual_inductive_body
 
-(***********************************************************************)
+(************************************************************************)
 (*s Modules *)
 val add_modtype : kernel_name -> module_type_body -> env -> env
 
@@ -118,14 +118,14 @@ val shallow_add_module : module_path -> module_body -> env -> env
 val lookup_module : module_path -> env -> module_body
 val lookup_modtype : kernel_name -> env -> module_type_body
 
-(***********************************************************************)
+(************************************************************************)
 (*s Universe constraints *)
 val set_universes   :   Univ.universes -> env -> env
 val add_constraints : Univ.constraints -> env -> env
 
 val set_engagement : engagement -> env -> env
 
-(***********************************************************************)
+(************************************************************************)
 (* Sets of referred section variables *)
 (* [global_vars_set env c] returns the list of [id]'s occurring as
    [VAR id] in [c] *)
@@ -135,7 +135,7 @@ val vars_of_global : env -> constr -> identifier list
 
 val keep_hyps : env -> Idset.t -> section_context
 
-(***********************************************************************)
+(************************************************************************)
 (*s Unsafe judgments. We introduce here the pre-type of judgments, which is
   actually only a datatype to store a term with its type and the type of its
   type. *)
diff --git a/kernel/esubst.ml b/kernel/esubst.ml
index a72f5a6349..7662a2f8ba 100644
--- a/kernel/esubst.ml
+++ b/kernel/esubst.ml
@@ -1,10 +1,10 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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        *)
+(************************************************************************)
 
 (* $Id$ *)
 
diff --git a/kernel/esubst.mli b/kernel/esubst.mli
index cbb5c37cc4..9f795d8577 100644
--- a/kernel/esubst.mli
+++ b/kernel/esubst.mli
@@ -1,10 +1,10 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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        *)
+(************************************************************************)
 
 (* $Id$ *)
 
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 1f357eb292..dbf7bc58e0 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -1,10 +1,10 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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        *)
+(************************************************************************)
 
 (* $Id$ *)
 
@@ -25,7 +25,7 @@ open Entries
    of names. The name [id] is the name of the current inductive type, used
    when reporting the error. *)
 
-(***********************************************************************)
+(************************************************************************)
 (* Various well-formedness check for inductive declarations            *)
 
 type inductive_error =
@@ -87,8 +87,8 @@ let mind_check_arities env mie =
     (fun {mind_entry_typename=id; mind_entry_arity=ar} -> check_arity id ar)
     mie.mind_entry_inds
 
-(***********************************************************************)
-(***********************************************************************)
+(************************************************************************)
+(************************************************************************)
 
 (* Typing the arities and constructor types *)
 
@@ -233,8 +233,8 @@ let typecheck_inductive env mie =
       ([],cst) in
   (env_arities, Array.of_list inds, cst)
 
-(***********************************************************************)
-(***********************************************************************)
+(************************************************************************)
+(************************************************************************)
 (* Positivity *)
 
 type ill_formed_ind =
@@ -446,8 +446,8 @@ let check_positivity env_ar inds =
   Rtree.mk_rec (Array.mapi check_one inds)
 
 
-(***********************************************************************)
-(***********************************************************************)
+(************************************************************************)
+(************************************************************************)
 (* Build the inductive packet *)
     
 (* Elimination sorts *)
@@ -536,8 +536,8 @@ let build_inductive env env_ar record finite inds recargs cst =
     mind_equiv = None;
   }
 
-(***********************************************************************)
-(***********************************************************************)
+(************************************************************************)
+(************************************************************************)
 
 let check_inductive env mie =
   (* First type-check the inductive definition *)
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 4e0f9012c0..bbfa47818d 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -1,10 +1,10 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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        *)
+(************************************************************************)
 
 (*i $Id$ i*)
 
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index fd1fa92db7..5b2e8998bf 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -1,10 +1,10 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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        *)
+(************************************************************************)
 
 (* $Id$ *)
 
@@ -45,7 +45,7 @@ let find_coinductive env c =
         when not (fst (lookup_mind_specif env ind)).mind_finite -> (ind, l)
     | _ -> raise Not_found
 
-(***********************************************************************)
+(************************************************************************)
 
 (* Build the substitution that replaces Rels by the appropriate *)
 (* inductives *)
@@ -86,8 +86,8 @@ let full_constructor_instantiate (((mind,_),mib,mip),params) =
   (fun t ->
     instantiate_params (inst_ind t) params mip.mind_params_ctxt)
 
-(***********************************************************************)
-(***********************************************************************)
+(************************************************************************)
+(************************************************************************)
 
 (* Functions to build standard types related to inductive *)
 
@@ -97,7 +97,7 @@ let type_of_inductive env i =
   let (_,mip) = lookup_mind_specif env i in
   mip.mind_user_arity
 
-(***********************************************************************)
+(************************************************************************)
 (* Type of a constructor *)
 
 let type_of_constructor env cstr =
@@ -118,7 +118,7 @@ let arities_of_constructors env ind =
 
 
 
-(***********************************************************************)
+(************************************************************************)
 
 let is_info_arity env c =
   match dest_arity env c with
@@ -214,7 +214,7 @@ let is_correct_arity env c pj ind mip params =
     error_elim_arity env ind listarity c pj kinds
 
 
-(***********************************************************************)
+(************************************************************************)
 (* Type of case branches *)
 
 (* [p] is the predicate, [i] is the constructor number (starting from 0),
@@ -254,7 +254,7 @@ let type_case_branches env (ind,largs) pj c =
   (lc, ty, univ)
 
 
-(***********************************************************************)
+(************************************************************************)
 (* Checking the case annotation is relevent *)
 
 let check_case_info env indsp ci =
@@ -264,8 +264,8 @@ let check_case_info env indsp ci =
     (mip.mind_nparams <> ci.ci_npar)
   then raise (TypeError(env,WrongCaseInfo(indsp,ci)))
 
-(***********************************************************************)
-(***********************************************************************)
+(************************************************************************)
+(************************************************************************)
 
 (* Guard conditions for fix and cofix-points *)
 
@@ -510,7 +510,7 @@ let check_is_subterm renv c ind =
     Subterm (Strict,_) | Dead_code -> true
   |  _ -> false
 
-(***********************************************************************)
+(************************************************************************)
 
 exception FixGuardError of env * guard_error
 
@@ -711,7 +711,7 @@ let cfkey = Profile.declare_profile "check_fix";;
 let check_fix env fix = Profile.profile3 cfkey check_fix env fix;;
 *)
 
-(***********************************************************************)
+(************************************************************************)
 (* Scrape *)
 
 let rec scrape_mind env kn = 
@@ -719,7 +719,7 @@ let rec scrape_mind env kn =
     | None -> kn
     | Some kn' -> scrape_mind env kn'
 
-(***********************************************************************)
+(************************************************************************)
 (* Co-fixpoints. *)
 
 exception CoFixGuardError of env * guard_error
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index a6ce7d42e8..0ecfe2a8c4 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -1,10 +1,10 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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        *)
+(************************************************************************)
 
 (*i $Id$ i*)
 
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 33eae08213..a96bc52fce 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -1,10 +1,10 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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        *)
+(************************************************************************)
 
 (*i $Id$ i*)
 
diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli
index 7d17d4823a..73dc914819 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___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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        *)
+(************************************************************************)
 
 (* $Id$ *)
 
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 569580bfb1..5a0694cbef 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -1,10 +1,10 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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        *)
+(************************************************************************)
 
 (*i $Id$ i*)
 
diff --git a/kernel/modops.mli b/kernel/modops.mli
index 1391380b19..f92c6bf042 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -1,10 +1,10 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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        *)
+(************************************************************************)
 
 (*i $Id$ i*)
 
diff --git a/kernel/names.ml b/kernel/names.ml
index cba4d9d627..68622703d6 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -1,10 +1,10 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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        *)
+(************************************************************************)
 
 (* $Id$ *)
 
diff --git a/kernel/names.mli b/kernel/names.mli
index 0e45778d0a..bd7b526873 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -1,10 +1,10 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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        *)
+(************************************************************************)
 
 (*i $Id$ i*)
 
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 5c57c50145..28628cbda7 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -1,10 +1,10 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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        *)
+(************************************************************************)
 
 (* $Id$ *)
 
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 63949ceb26..4f519fff7a 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -1,10 +1,10 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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        *)
+(************************************************************************)
 
 (*i $Id$ i*)
 
@@ -13,7 +13,7 @@ open Term
 open Environ
 (*i*)
 
-(***********************************************************************)
+(************************************************************************)
 (*s Reduction functions *)
 
 val whd_betaiotazeta        : env -> constr -> constr
@@ -22,7 +22,7 @@ val whd_betadeltaiota_nolet : env -> constr -> constr
 
 val nf_betaiota      : constr -> constr
 
-(***********************************************************************)
+(************************************************************************)
 (*s conversion functions *)
 
 exception NotConvertible
@@ -36,7 +36,7 @@ val conv           : types conversion_function
 val conv_leq       : types conversion_function
 val conv_leq_vecti : types array conversion_function
 
-(***********************************************************************)
+(************************************************************************)
 
 (* Builds an application node, reducing beta redexes it may produce. *) 
 val beta_appvect : constr -> constr array -> constr
@@ -45,7 +45,7 @@ val beta_appvect : constr -> constr array -> constr
 val hnf_prod_applist : env -> types -> constr list -> types
 
 
-(***********************************************************************)
+(************************************************************************)
 (*s Recognizing products and arities modulo reduction *)
 
 val dest_prod       : env -> types -> Sign.rel_context * types
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index d007af08eb..0182b39073 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -1,10 +1,10 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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        *)
+(************************************************************************)
 
 (* $Id$ *)
 
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 86e423dd83..f59b5c3756 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___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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        *)
+(************************************************************************)
 
 (*i $Id$ i*)
 
diff --git a/kernel/sign.ml b/kernel/sign.ml
index 40f6e46ad1..d448ea3100 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -1,10 +1,10 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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        *)
+(************************************************************************)
 
 (* $Id$ *)
 
diff --git a/kernel/sign.mli b/kernel/sign.mli
index 196d81ca3b..2bb921fe1e 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -1,10 +1,10 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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        *)
+(************************************************************************)
 
 (*i $Id$ i*)
 
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 099e93117a..6bd88c8cd0 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -1,10 +1,10 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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        *)
+(************************************************************************)
 
 (*i $Id$ i*)
 
diff --git a/kernel/subtyping.mli b/kernel/subtyping.mli
index 71c1113391..c0b1ee5d3c 100644
--- a/kernel/subtyping.mli
+++ b/kernel/subtyping.mli
@@ -1,10 +1,10 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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        *)
+(************************************************************************)
 
 (*i $Id$ i*)
 
diff --git a/kernel/term.ml b/kernel/term.ml
index 736734365e..08bcd1ddd2 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -1,10 +1,10 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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        *)
+(************************************************************************)
 
 (* $Id$ *)
 
@@ -256,9 +256,9 @@ let mkCoFix cofix = CoFix cofix
 
 let kind_of_term c = c
 
-(***********************************************************************)
+(************************************************************************)
 (*    kind_of_term = constructions as seen by the user                 *)
-(***********************************************************************)
+(************************************************************************)
 
 (* User view of [constr]. For [App], it is ensured there is at
    least one argument and the function is not itself an applicative
diff --git a/kernel/term.mli b/kernel/term.mli
index 629d3c999a..8c72a9ff30 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -1,10 +1,10 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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        *)
+(************************************************************************)
 
 (*i $Id$ i*)
 
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 0860b95eed..b2ecfa5990 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -1,10 +1,10 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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        *)
+(************************************************************************)
 
 (* $Id$ *)
 
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 4fb104c02f..74dc9dc8c2 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___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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        *)
+(************************************************************************)
 
 (*i $Id$ i*)
 
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index c0538c36a0..73aaaed937 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -1,10 +1,10 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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        *)
+(************************************************************************)
 
 (* $Id$ *)
 
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index b4897d6127..f9f2e04a48 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___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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        *)
+(************************************************************************)
 
 (*i $Id$ i*)
 
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 46ee8d97e1..46cf163bf0 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -1,10 +1,10 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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        *)
+(************************************************************************)
 
 (* $Id$ *)
 
@@ -319,8 +319,8 @@ let type_fixpoint env lna lar vdefj =
   with NotConvertibleVect i ->
     error_ill_typed_rec_body env i lna vdefj lar
 
-(***********************************************************************)
-(***********************************************************************)
+(************************************************************************)
+(************************************************************************)
 
 (* This combinator adds the universe constraints both in the local
    graph and in the universes of the environment. This is to ensure
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 55adf86a20..a537d793eb 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -1,10 +1,10 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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        *)
+(************************************************************************)
 
 (*i $Id$ i*)
 
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 9242e9d8a1..b734877a5b 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1,10 +1,10 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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        *)
+(************************************************************************)
 
 (* $Id$ *)
 
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 0da9b79dfb..990460f9bb 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -1,10 +1,10 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \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        *)
+(************************************************************************)
 
 (*i $Id$ i*)
 
-- 
cgit v1.2.3