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
---
 pretyping/coercion.ml  |  9 +++++++++
 pretyping/pretyping.ml | 15 +++++++++++++++
 pretyping/recordops.ml |  7 +++++++
 3 files changed, 31 insertions(+)

(limited to 'pretyping')

diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index f2975d21c0..cc064cd67b 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -5,6 +5,15 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
+
+(* Created by Hugo Herbelin for Coq V7 by isolating the coercion
+   mechanism out of the type inference algorithm in file trad.ml from
+   Coq V6.3, Nov 1999; The coercion mechanism was implemented in
+   trad.ml by Amokrane Saïbi, May 1996 *)
+(* Addition of products and sorts in canonical structures by Pierre
+   Corbineau, Feb 2008 *)
+(* Turned into an abstract compilation unit by Matthieu Sozeau, March 2006 *)
+
 open Util
 open Names
 open Term
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 92968cad90..70241238db 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -6,6 +6,21 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(* This file contains the syntax-directed part of the type inference
+   algorithm introduced by Murthy in Coq V5.10, 1995; the type
+   inference algorithm was initially developed in a file named trad.ml
+   which formerly contained a simple concrete-to-abstract syntax
+   translation function introduced in CoC V4.10 for implementing the
+   "exact" tactic, 1989 *)
+(* Support for typing term in Ltac environment by David Delahaye, 2000 *)
+(* Type inference algorithm made a functor of the coercion and
+   pattern-matching compilation by Matthieu Sozeau, March 2006 *)
+(* Fixpoint guard index computation by Pierre Letouzey, July 2007 *)
+
+(* Structural maintainer: Hugo Herbelin *)
+(* Secondary maintenance: collective *)
+
+
 open Pp
 open Util
 open Names
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 32433f6be6..df0f3e460e 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -6,6 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(* Created by Amokrane Saïbi, Dec 1998 *)
+(* Addition of products and sorts in canonical structures by Pierre
+   Corbineau, Feb 2008 *)
+
+(* This file registers properties of records: projections and
+   canonical structures *)
+
 open Util
 open Pp
 open Names
-- 
cgit v1.2.3