diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/coercion.ml | 9 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 15 | ||||
| -rw-r--r-- | pretyping/recordops.ml | 7 |
3 files changed, 31 insertions, 0 deletions
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 |