From bf8f56f2a19fab3c7de947c0dc928e7b4f4ac6ff Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 9 May 2010 14:48:55 +0000
Subject: Added a few informations about file lineages (for the most part in
 kernel)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13005 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/cbytecodes.ml     | 16 +++++++++++++++
 kernel/cbytecodes.mli    | 10 ++++++++++
 kernel/cbytegen.ml       | 46 ++++++++++++++++++++++++++++---------------
 kernel/cemitcodes.ml     | 14 +++++++++++++
 kernel/closure.ml        | 13 ++++++++++++
 kernel/conv_oracle.ml    |  3 +++
 kernel/cooking.ml        |  7 +++++++
 kernel/csymtable.ml      | 16 +++++++++++++++
 kernel/csymtable.mli     | 10 ++++++++++
 kernel/declarations.ml   | 21 ++++++++++++++------
 kernel/environ.ml        | 14 +++++++++++++
 kernel/esubst.ml         |  4 ++++
 kernel/mod_subst.ml      |  7 +++++++
 kernel/mod_typing.ml     |  6 ++++++
 kernel/modops.ml         | 13 ++++++++----
 kernel/names.ml          | 12 ++++++++++++
 kernel/pre_env.ml        |  7 +++++++
 kernel/reduction.ml      |  9 +++++++++
 kernel/retroknowledge.ml |  7 +++++++
 kernel/safe_typing.ml    | 51 ++++++++++++++++++++++++++++++++++++++++++++++++
 kernel/sign.ml           |  9 +++++++++
 kernel/subtyping.ml      |  7 +++++--
 kernel/term.ml           | 18 +++++++++++++++--
 kernel/term_typing.ml    |  6 ++++++
 kernel/univ.ml           |  7 +++++--
 25 files changed, 301 insertions(+), 32 deletions(-)

(limited to 'kernel')

diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index f4d0bb2b22..ae58a4dc0c 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -1,3 +1,19 @@
+(************************************************************************)
+(*  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$ *)
+
+(* Created by Bruno Barras for Benjamin Grégoire as part of the
+   bytecode-based reduction machine, Oct 2004 *)
+(* Support for native arithmetics by Arnaud Spiwack, May 2007 *)
+
+(* This file defines the type of bytecode instructions *)
+
 open Names
 open Term
 
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index a8860d6d80..a539093f00 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -1,3 +1,13 @@
+(************************************************************************)
+(*  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$ *)
+
 open Names
 open Term
 
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 68ee15ab7c..68f0d7936d 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -1,3 +1,17 @@
+(************************************************************************)
+(*  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$ *)
+
+(* Author: Benjamin Grégoire as part of the bytecode-based virtual reduction
+   machine, Oct 2004 *)
+(* Extension: Arnaud Spiwack (support for native arithmetic), May 2005 *)
+
 open Util
 open Names
 open Cbytecodes
@@ -7,15 +21,15 @@ open Declarations
 open Pre_env
 
 
-(* Compilation des variables + calcul des variables libres               *)
+(* Compilation des variables + calcul des variables libres                *)
 
-(* Dans la machine virtuel il n'y a pas de difference entre les           *)
+(* Dans la machine virtuelle il n'y a pas de difference entre les         *)
 (* fonctions et leur environnement                                        *)
 
-(* Representation de l'environnements des fonctions :                     *)
+(* Representation de l'environnement des fonctions :                      *)
 (*        [clos_t | code | fv1 | fv2 | ... | fvn ]                        *)
 (*                ^                                                       *)
-(*  l'offset pour l'acces au variable libre est 1 (il faut passer le      *)
+(*  l'offset pour l'acces aux variables libres est 1 (il faut passer le   *)
 (*  pointeur de code).                                                    *)
 (*  Lors de la compilation, les variables libres sont stock'ees dans      *)
 (*  [in_env] dans l'ordre inverse de la representation machine, ceci      *)
@@ -28,21 +42,21 @@ open Pre_env
 (* Dans le corps de la fonction [arg1] est repr'esent'e par le de Bruijn  *)
 (*  [n], [argn] par le de Bruijn [1]                                      *)
 
-(* Representation des environnements des points fix mutuels :             *)
+(* Representation des environnements des points fixes mutuels :           *)
 (* [t1|C1| ... |tc|Cc| ... |t(nbr)|C(nbr)| fv1 | fv2 | .... | fvn | type] *)
 (*                ^<----------offset--------->                            *)
 (* type = [Ct1 | .... | Ctn]                                              *)
-(* Ci est le code correspondant au corps du ieme point fix                *)
-(* Lors de l'evaluation d'un point fix l'environnement est un pointeur    *)
+(* Ci est le code correspondant au corps du ieme point fixe               *)
+(* Lors de l'evaluation d'un point fixe l'environnement est un pointeur   *)
 (* sur la position correspondante a son code.                             *)
-(* Dans le corps de chaque point fix le de Bruijn [nbr] represente,       *)
-(* le 1er point fix de la declaration mutuelle, le de Bruijn [1] le       *)
+(* Dans le corps de chaque point fixe le de Bruijn [nbr] represente,      *)
+(* le 1er point fixe de la declaration mutuelle, le de Bruijn [1] le      *)
 (* nbr-ieme.                                                              *)
 (* L'acces a ces variables se fait par l'instruction [Koffsetclosure]     *)
 (*  (decalage de l'environnement)                                         *)
 
-(* Ceci permet de representer tout les point fix mutuels en un seul bloc  *)
-(* [Ct1 | ... | Ctn] est un tableau contant le code d'evaluation des      *)
+(* Ceci permet de representer les points fixes mutuels en un seul bloc    *)
+(* [Ct1 | ... | Ctn] est un tableau contenant le code d'evaluation des    *)
 (* types des points fixes, ils sont utilises pour tester la conversion    *)
 (* Leur environnement d'execution est celui du dernier point fix :        *)
 (* [t1|C1| ... |tc|Cc| ... |t(nbr)|C(nbr)| fv1 | fv2 | .... | fvn | type] *)
@@ -59,7 +73,7 @@ open Pre_env
 (*                ...                                                     *)
 (*  fcofixnbr = [clos_t | codenbr | a1 |...| anbr | fv1 |...| fvn | type] *)
 (*                      ^                                                 *)
-(*  Les block [ai] sont des fonctions qui accumulent leurs arguments :    *)
+(*  Les blocs [ai] sont des fonctions qui accumulent leurs arguments :    *)
 (*           ai arg1  argp --->                                           *)
 (*    ai' = [A_t | accumulate | [Cfx_t | fcofixi] | arg1 | ... | argp ]   *)
 (* Si un tel bloc arrive sur un [match] il faut forcer l'evaluation,      *)
@@ -68,10 +82,10 @@ open Pre_env
 (* l'evaluation :                                                         *)
 (*  ai' <--                                                               *)
 (*   [A_t | accumulate | [Cfxe_t |fcofixi|result] | arg1 | ... | argp ]   *)
-(* L'avantage de cette representation est qu'elle permet d'evaluer qu'une *)
-(* fois l'application d'un cofix (evaluation lazy)                        *)
-(* De plus elle permet de creer facilement des cycles quand les cofix ne  *)
-(* n'ont pas d'aruments, ex:                                              *)
+(* L'avantage de cette representation est qu'elle permet de n'evaluer     *)
+(* qu'une fois l'application d'un cofix (evaluation lazy)                 *)
+(* De plus elle permet de creer facilement des cycles quand les cofix     *)
+(* n'ont pas d'argument, ex:                                              *)
 (*   cofix one := cons 1 one                                              *)
 (*   a1 = [A_t | accumulate | [Cfx_t|fcofix1] ]                           *)
 (*   fcofix1 = [clos_t | code | a1]                                       *)
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 4a9c7da2b5..962417c1e9 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -1,3 +1,17 @@
+(************************************************************************)
+(*  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:$ *)
+
+(* Author: Benjamin Grégoire as part of the bytecode-based virtual reduction
+   machine, Oct 2004 *)
+(* Extension: Arnaud Spiwack (support for native arithmetic), May 2005 *)
+
 open Names
 open Term
 open Cbytecodes
diff --git a/kernel/closure.ml b/kernel/closure.ml
index e77ea4cb33..86a42dc630 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -6,6 +6,19 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(* Created by Bruno Barras with Benjamin Werner's account to implement
+   a call-by-value conversion algorithm and a lazy reduction machine
+   with sharing, Nov 1996 *)
+(* Addition of zeta-reduction (let-in contraction) by Hugo Herbelin, Oct 2000 *)
+(* Call-by-value machine moved to cbv.ml, Mar 01 *)
+(* Additional tools for module subtyping by Jacek Chrzaszcz, Aug 2002 *)
+(* Extension with closure optimization by Bruno Barras, Aug 2003 *)
+(* Support for evar reduction by Bruno Barras, Feb 2009 *)
+(* Miscellaneous other improvements by Bruno Barras, 1997-2009 *)
+
+(* This file implements a lazy reduction for the Calculus of Inductive
+   Constructions *)
+
 open Util
 open Pp
 open Term
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index 5e9db9c7d2..edb03ecf57 100644
--- a/kernel/conv_oracle.ml
+++ b/kernel/conv_oracle.ml
@@ -6,6 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(* Created by Bruno Barras as part of the rewriting of the conversion
+   algorithm, Nov 2001 *)
+
 open Names
 
 (* Priority for the expansion of constant in the conversion test.
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 7b380944bf..243efa795b 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -6,6 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(* Created by Jean-Christophe Filliâtre out of V6.3 file constants.ml
+   as part of the rebuilding of Coq around a purely functional
+   abstract type-checker, Nov 1999 *)
+
+(* This module implements kernel-level discharching of local
+   declarations over global constants and inductive types *)
+
 open Pp
 open Util
 open Names
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 145ca27d2e..1c1645e971 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -1,3 +1,19 @@
+(************************************************************************)
+(*  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$ *)
+
+(* Created by Bruno Barras for Benjamin Grégoire as part of the
+   bytecode-based reduction machine, Oct 2004 *)
+(* Bug fix #1419 by Jean-Marc Notin, Mar 2007 *)
+
+(* This file manages the table of global symbols for the bytecode machine *)
+
 open Names
 open Term
 open Vm
diff --git a/kernel/csymtable.mli b/kernel/csymtable.mli
index 894a33ef5b..160011f0b9 100644
--- a/kernel/csymtable.mli
+++ b/kernel/csymtable.mli
@@ -1,3 +1,13 @@
+(************************************************************************)
+(*  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$ *)
+
 open Names
 open Term
 open Pre_env
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 0762a92d19..4f98bb8b07 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -6,21 +6,30 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i*)
+(* This file is a late renaming in May 2000 of constant.ml which
+   itself was made for V7.0 in Aug 1999 out of a dispatch by
+   Jean-Christophe Filliâtre of Chet Murthy's constants.ml in V5.10.5
+   into cooking.ml, declare.ml and constant.ml, ...; renaming done
+   because the new contents exceeded in extent what the name
+   suggested *)
+(* Cleaning and lightening of the kernel by Bruno Barras, Nov 2001 *)
+(* Declarations for the module systems added by Jacek Chrzaszcz, Aug 2002 *)
+(* Miscellaneous extensions, cleaning or restructurations by Bruno
+   Barras, Hugo Herbelin, Jean-Christophe Filliâtre, Pierre Letouzey *)
+
+(* This module defines the types of global declarations. This includes
+   global constants/axioms, mutual inductive definitions and the
+   module system *)
+
 open Util
 open Names
 open Univ
 open Term
 open Sign
 open Mod_subst
-(*i*)
-
-(* This module defines the types of global declarations. This includes
-   global constants/axioms and mutual inductive definitions *)
 
 type engagement = ImpredicativeSet
 
-
 (*s Constants (internal representation) (Definition/Axiom) *)
 
 type polymorphic_arity = {
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 69220908ef..29374d24c5 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -6,6 +6,20 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(* Author: Jean-Christophe Filliâtre as part of the rebuilding of Coq
+   around a purely functional abstract type-checker, Aug 1999 *)
+(* Cleaning and lightening of the kernel by Bruno Barras, Nov 2001 *)
+(* Flag for predicativity of Set by Hugo Herbelin in Oct 2003 *)
+(* Support for virtual machine by Benjamin Grégoire in Oct 2004 *)
+(* Support for retroknowledge by Arnaud Spiwack in May 2007 *)
+(* Support for assumption dependencies by Arnaud Spiwack in May 2007 *)
+
+(* Miscellaneous maintenance by Bruno Barras, Hugo Herbelin, Jean-Marc
+   Notin, Matthieu Sozeau *)
+
+(* This file defines the type of environments on which the
+   type-checker works, together with simple related functions *)
+
 open Util
 open Names
 open Sign
diff --git a/kernel/esubst.ml b/kernel/esubst.ml
index fd07d92971..04e0f507ed 100644
--- a/kernel/esubst.ml
+++ b/kernel/esubst.ml
@@ -6,6 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(* Created by Bruno Barras for Coq V7.0, Mar 2001 *)
+
+(* Support for explicit substitutions *)
+
 open Util
 
 (*********************)
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 8abfe09437..c967bf1bac 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -6,6 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(* Created by Claudio Sacerdoti from contents of term.ml, names.ml and
+   new support for constant inlining in functor application, Nov 2004 *)
+(* Optimizations and bug fixes by Élie Soubiran, from Feb 2008 *)
+
+(* This file provides types and functions for managing name
+   substitution in module constructions *)
+
 open Pp
 open Util
 open Names
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index e67b987a6f..b2e199ff8b 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -6,6 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(* Created by Jacek Chrzaszcz, Aug 2002 as part of the implementation of
+   the Coq module system *)
+
+(* This module provides the main functions for type-checking module
+   declarations *)
+
 open Util
 open Names
 open Univ
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 084fdd4f41..38f59abe3d 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -6,7 +6,15 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i*)
+(* Created by Jacek Chrzaszcz, Aug 2002 as part of the implementation of
+   the Coq module system *)
+(* Inlining and more liberal use of modules and module types by Claudio
+   Sacerdoti, Nov 2004 *)
+(* New structure-based model of modules and miscellaneous bug fixes by
+   Élie Soubiran, from Feb 2008 *)
+
+(* This file provides with various operations on modules and module types *)
+
 open Util
 open Pp
 open Names
@@ -16,9 +24,6 @@ open Declarations
 open Environ
 open Entries
 open Mod_subst
-(*i*)
-
-
 
 let error_existing_label l = 
   error ("The label "^string_of_label l^" is already declared.")
diff --git a/kernel/names.ml b/kernel/names.ml
index 463f47ca4c..d5f301f2f0 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -6,6 +6,18 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(* File created around Apr 1994 for CiC V5.10.5 by Chet Murthy collecting
+   parts of file initial.ml from CoC V4.8, Dec 1988, by Gérard Huet,
+   Thierry Coquand and Christine Paulin *)
+(* Hash-consing by Bruno Barras in Feb 1998 *)
+(* Extra functions for splitting/generation of identifiers by Hugo Herbelin *)
+(* Restructuration by Jacek Chrzaszcz as part of the implementation of
+   the module system, Aug 2002 *)
+(* Abstraction over the type of constant for module inlining by Claudio
+   Sacerdoti, Nov 2004 *)
+(* Miscellaneous features or improvements by Hugo Herbelin, 
+   Élie Soubiran, ... *)
+
 open Pp
 open Util
 
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 3835c81c51..d964ad1ba3 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -6,6 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(* Created by Benjamin Grégoire out of environ.ml for better
+   modularity in the design of the bytecode virtual evaluation
+   machine, Dec 2005 *)
+(* Bug fix by Jean-Marc Notin *)
+
+(* This file defines the type of kernel environments *)
+
 open Util
 open Names
 open Sign
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 4a4661f996..e215f23361 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -6,6 +6,15 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(* Created under Benjamin Werner account by Bruno Barras to implement
+   a call-by-value conversion algorithm and a lazy reduction machine
+   with sharing, Nov 1996 *)
+(* Addition of zeta-reduction (let-in contraction) by Hugo Herbelin, Oct 2000 *)
+(* Irreversibility of opacity by Bruno Barras *)
+(* Cleaning and lightening of the kernel by Bruno Barras, Nov 2001 *)
+(* Equal inductive types by Jacek Chrzaszcz as part of the module
+   system, Aug 2002 *)
+
 open Util
 open Names
 open Term
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index c0f714f96c..1dfafc08f7 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -6,6 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(* Created by Arnaud Spiwack, May 2007 *)
+(* Addition of native Head (nb of heading 0) and Tail (nb of trailing 0) by
+   Benjamin Grégoire, Jun 2007 *)
+
+(* This file defines the knowledge that the kernel is able to optimize
+   for evaluation in the bytecode virtual machine *)
+
 open Term
 open Names
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index cffe7e7722..6a18f72d5c 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -6,6 +6,57 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(* Created by Jean-Christophe Filliâtre as part of the rebuilding of
+   Coq around a purely functional abstract type-checker, Dec 1999 *)
+
+(* This file provides the entry points to the kernel type-checker. It
+   defines the abstract type of well-formed environments and
+   implements the rules that build well-formed environments.
+
+   An environment is made of constants and inductive types (E), of
+   section declarations (Delta), of local bound-by-index declarations
+   (Gamma) and of universe constraints (C). Below E[Delta,Gamma] |-_C
+   means that the tuple E, Delta, Gamma, C is a well-formed
+   environment. Main rules are:
+
+   empty_environment:
+
+     ------
+     [,] |-
+
+   push_named_assum(a,T):
+   
+     E[Delta,Gamma] |-_G
+     ------------------------
+     E[Delta,Gamma,a:T] |-_G'
+
+   push_named_def(a,t,T):
+   
+     E[Delta,Gamma] |-_G
+     ---------------------------
+     E[Delta,Gamma,a:=t:T] |-_G'
+
+   add_constant(ConstantEntry(DefinitionEntry(c,t,T))):
+
+     E[Delta,Gamma] |-_G
+     ---------------------------
+     E,c:=t:T[Delta,Gamma] |-_G'
+
+   add_constant(ConstantEntry(ParameterEntry(c,T))):
+
+     E[Delta,Gamma] |-_G
+     ------------------------
+     E,c:T[Delta,Gamma] |-_G'
+
+   add_mind(Ind(Ind[Gamma_p](Gamma_I:=Gamma_C))):
+
+     E[Delta,Gamma] |-_G
+     ------------------------
+     E,Ind[Gamma_p](Gamma_I:=Gamma_C)[Delta,Gamma] |-_G'
+
+   etc.
+*)
+
 open Util
 open Names
 open Univ
diff --git a/kernel/sign.ml b/kernel/sign.ml
index f987a1f6c9..43151d98c8 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -6,6 +6,15 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(* Created by Jean-Christophe Filliâtre out of names.ml as part of the
+   rebuilding of Coq around a purely functional abstract type-checker,
+   Aug 1999 *)
+(* Miscellaneous extensions, restructurations and bug-fixes by Hugo
+   Herbelin and Bruno Barras *)
+
+(* This file defines types and combinators regarding indexes-based and
+   names-based contexts *)
+
 open Names
 open Util
 open Term
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 9bc719e7e7..1b535ea430 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -6,6 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(* Created by Jacek Chrzaszcz, Aug 2002 as part of the implementation of
+   the Coq module system *)
+
+(* This module checks subtyping of module types *)
+
 (*i*)
 open Util
 open Names
@@ -20,8 +25,6 @@ open Mod_subst
 open Entries
 (*i*)
 
-
-
 (* This local type is used to subtype a constant with a constructor or
    an inductive type. It can also be useful to allow reorderings in
    inductive types *)
diff --git a/kernel/term.ml b/kernel/term.ml
index a1effb317e..5f1c031886 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -6,7 +6,22 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* This module instantiates the structure of generic deBruijn terms to Coq *)
+(* File initially created by Gérard Huet and Thierry Coquand in 1984 *)
+(* Extension to inductive constructions by Christine Paulin for Coq V5.6 *)
+(* Extension to mutual inductive constructions by Christine Paulin for
+   Coq V5.10.2 *)
+(* Extension to co-inductive constructions by Eduardo Gimenez *)
+(* Optimization of substitution functions by Chet Murthy *)
+(* Optimization of lifting functions by Bruno Barras, Mar 1997 *)
+(* Hash-consing by Bruno Barras in Feb 1998 *)
+(* Restructuration of Coq of the type-checking kernel by Jean-Christophe 
+   Filliâtre, 1999 *)
+(* Abstraction of the syntax of terms and iterators by Hugo Herbelin, 2000 *)
+(* Cleaning and lightening of the kernel by Bruno Barras, Nov 2001 *)
+
+(* This file defines the internal syntax of the Calculus of
+   Inductive Constructions (CIC) terms together with constructors,
+   destructors, iterators and basic functions *)
 
 open Util
 open Pp
@@ -14,7 +29,6 @@ open Names
 open Univ
 open Esubst
 
-(* Coq abstract syntax with deBruijn variables; 'a is the type of sorts *)
 
 type existential_key = int
 type metavariable = int
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index dac8ee47af..da33930657 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -6,6 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(* Created by Jacek Chrzaszcz, Aug 2002 as part of the implementation of
+   the Coq module system *)
+
+(* This module provides the main entry points for type-checking basic
+   declarations *)
+
 open Util
 open Names
 open Univ
diff --git a/kernel/univ.ml b/kernel/univ.ml
index f42b6fb939..ca0d8fbd03 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -6,10 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* Initial Caml version originates from CoC 4.8 [Dec 1988] *)
-(* Extension with algebraic universes by HH [Sep 2001] *)
+(* Created in Caml by Gérard Huet for CoC 4.8 [Dec 1988] *)
+(* Functional code by Jean-Christophe Filliâtre for Coq V7.0 [1999] *)
+(* Extension with algebraic universes by HH for Coq V7.0 [Sep 2001] *)
 (* Additional support for sort-polymorphic inductive types by HH [Mar 2006] *)
 
+(* Revisions by Bruno Barras, Hugo Herbelin, Pierre Letouzey *)
+
 (* Universes are stratified by a partial ordering $\le$.
    Let $\~{}$ be the associated equivalence. We also have a strict ordering
    $<$ between equivalence classes, and we maintain that $<$ is acyclic,
-- 
cgit v1.2.3