Nouvelle en-tête

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

42 files changed, 337 insertions, 337 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 1d85089e9..f4db948a0 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 e045bd60f..e0cfe7b51 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 527030fb4..11d4435c2 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 0eefb8711..8dad2e2bd 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 7c3b8e60f..c37c81cf6 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 b54189ba6..7bd64d326 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 0aa5c9948..152c1e5bf 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 7c6d3ecdf..a168abdfb 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 e383dbabd..4d485ff8c 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 e383dbabd..4d485ff8c 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 9d81e8f00..41b664309 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 540fd02d3..71fc8e6d8 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 a72f5a634..7662a2f8b 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 cbb5c37cc..9f795d857 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 1f357eb29..dbf7bc58e 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 4e0f9012c..bbfa47818 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 fd1fa92db..5b2e8998b 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 a6ce7d42e..0ecfe2a8c 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 33eae0821..a96bc52fc 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 7d17d4823..73dc91481 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 569580bfb..5a0694cbe 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 1391380b1..f92c6bf04 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 cba4d9d62..68622703d 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 0e45778d0..bd7b52687 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 5c57c5014..28628cbda 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 63949ceb2..4f519fff7 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 d007af08e..0182b3907 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 86e423dd8..f59b5c375 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 40f6e46ad..d448ea310 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 196d81ca3..2bb921fe1 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 099e93117..6bd88c8cd 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 71c111339..c0b1ee5d3 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 736734365..08bcd1ddd 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 629d3c999..8c72a9ff3 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 0860b95ee..b2ecfa599 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 4fb104c02..74dc9dc8c 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 c0538c36a..73aaaed93 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 b4897d612..f9f2e04a4 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 46ee8d97e..46cf163bf 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 55adf86a2..a537d793e 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 9242e9d8a..b734877a5 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 0da9b79df..990460f9b 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*)