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

7 files changed, 25 insertions, 0 deletions

diff --git a/theories/Logic/Classical.v b/theories/Logic/Classical.v
index 4a01f3fae5..e75bfb4e6d 100644
--- a/theories/Logic/Classical.v
+++ b/theories/Logic/Classical.v
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(* File created for Coq V5.10.14b, Oct 1995 *)
+
 (** Classical Logic *)
 
 Require Export Classical_Prop.
diff --git a/theories/Logic/Classical_Pred_Set.v b/theories/Logic/Classical_Pred_Set.v
index afbb5e6dfc..f6c6446b47 100644
--- a/theories/Logic/Classical_Pred_Set.v
+++ b/theories/Logic/Classical_Pred_Set.v
@@ -6,6 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(* File created for Coq V5.10.14b, Oct 1995, by duplication of
+   Classical_Pred_Type.v *)
+
 (** This file is obsolete, use Classical_Pred_Type.v via Classical.v
 instead *)
 
diff --git a/theories/Logic/Classical_Pred_Type.v b/theories/Logic/Classical_Pred_Type.v
index 45c487cf7b..18ed260d46 100644
--- a/theories/Logic/Classical_Pred_Type.v
+++ b/theories/Logic/Classical_Pred_Type.v
@@ -6,6 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(* This file is a renaming for V5.10.14b, Oct 1995, of file Classical.v
+   introduced in Coq V5.8.3, June 1993 *)
+
 (** Classical Predicate Logic on Type *)
 
 Require Import Classical_Prop.
diff --git a/theories/Logic/Classical_Prop.v b/theories/Logic/Classical_Prop.v
index ee6dd96f2a..24544b908a 100644
--- a/theories/Logic/Classical_Prop.v
+++ b/theories/Logic/Classical_Prop.v
@@ -6,6 +6,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(* File created for Coq V5.10.14b, Oct 1995 *)
+(* Classical tactics for proving disjunctions by Julien Narboux, Jul 2005 *)
+(* Inferred proof-irrelevance and eq_rect_eq added by Hugo Herbelin, Mar 2006 *)
+
 (** Classical Propositional Logic *)
 
 Require Import ClassicalFacts.
diff --git a/theories/Logic/Eqdep.v b/theories/Logic/Eqdep.v
index 14ab70b67c..406429ffdf 100644
--- a/theories/Logic/Eqdep.v
+++ b/theories/Logic/Eqdep.v
@@ -7,6 +7,10 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(* File Eqdep.v created by Christine Paulin-Mohring in Coq V5.6, May 1992 *)
+(* Abstraction with respect to the eq_rect_eq axiom and creation of
+   EqdepFacts.v by Hugo Herbelin, Mar 2006 *)
+
 (** This file axiomatizes the invariance by substitution of reflexive
     equality proofs [[Streicher93]] and exports its consequences, such
     as the injectivity of the projection of the dependent pair.
diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v
index 9c20905c76..d542ecdb10 100644
--- a/theories/Logic/EqdepFacts.v
+++ b/theories/Logic/EqdepFacts.v
@@ -7,6 +7,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(* File Eqdep.v created by Christine Paulin-Mohring in Coq V5.6, May 1992 *)
+(* Further documentation and variants of eq_rect_eq by Hugo Herbelin,
+   Apr 2003 *)
+(* Abstraction with respect to the eq_rect_eq axiom and renaming to
+   EqdepFacts.v by Hugo Herbelin, Mar 2006 *)
+
 (** This file defines dependent equality and shows its equivalence with
     equality on dependent pairs (inhabiting sigma-types). It derives
     the consequence of axiomatizing the invariance by substitution of
diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v
index d4d05fe1a7..d10d6ff955 100644
--- a/theories/Logic/Eqdep_dec.v
+++ b/theories/Logic/Eqdep_dec.v
@@ -6,6 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(* Created by Bruno Barras, Jan 1998 *)
+(* Made a module instance for EqdepFacts by Hugo Herbelin, Mar 2006 *)
+
 (** We prove that there is only one proof of [x=x], i.e [refl_equal x].
     This holds if the equality upon the set of [x] is decidable.
     A corollary of this theorem is the equality of the right projections