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

1 files changed, 16 insertions, 2 deletions

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