From bf8f56f2a19fab3c7de947c0dc928e7b4f4ac6ff Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
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/declarations.ml | 21 +++++++++++++++------
 1 file changed, 15 insertions(+), 6 deletions(-)

(limited to 'kernel/declarations.ml')

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 0762a92d1..4f98bb8b0 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 = {
-- 
cgit v1.2.3