diff options
35 files changed, 357 insertions, 32 deletions
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index f4d0bb2b2..ae58a4dc0 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -1,3 +1,19 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +(* Created by Bruno Barras for Benjamin Grégoire as part of the + bytecode-based reduction machine, Oct 2004 *) +(* Support for native arithmetics by Arnaud Spiwack, May 2007 *) + +(* This file defines the type of bytecode instructions *) + open Names open Term diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index a8860d6d8..a539093f0 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -1,3 +1,13 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + open Names open Term diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 68ee15ab7..68f0d7936 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -1,3 +1,17 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +(* Author: Benjamin Grégoire as part of the bytecode-based virtual reduction + machine, Oct 2004 *) +(* Extension: Arnaud Spiwack (support for native arithmetic), May 2005 *) + open Util open Names open Cbytecodes @@ -7,15 +21,15 @@ open Declarations open Pre_env -(* Compilation des variables + calcul des variables libres *) +(* Compilation des variables + calcul des variables libres *) -(* Dans la machine virtuel il n'y a pas de difference entre les *) +(* Dans la machine virtuelle il n'y a pas de difference entre les *) (* fonctions et leur environnement *) -(* Representation de l'environnements des fonctions : *) +(* Representation de l'environnement des fonctions : *) (* [clos_t | code | fv1 | fv2 | ... | fvn ] *) (* ^ *) -(* l'offset pour l'acces au variable libre est 1 (il faut passer le *) +(* l'offset pour l'acces aux variables libres est 1 (il faut passer le *) (* pointeur de code). *) (* Lors de la compilation, les variables libres sont stock'ees dans *) (* [in_env] dans l'ordre inverse de la representation machine, ceci *) @@ -28,21 +42,21 @@ open Pre_env (* Dans le corps de la fonction [arg1] est repr'esent'e par le de Bruijn *) (* [n], [argn] par le de Bruijn [1] *) -(* Representation des environnements des points fix mutuels : *) +(* Representation des environnements des points fixes mutuels : *) (* [t1|C1| ... |tc|Cc| ... |t(nbr)|C(nbr)| fv1 | fv2 | .... | fvn | type] *) (* ^<----------offset---------> *) (* type = [Ct1 | .... | Ctn] *) -(* Ci est le code correspondant au corps du ieme point fix *) -(* Lors de l'evaluation d'un point fix l'environnement est un pointeur *) +(* Ci est le code correspondant au corps du ieme point fixe *) +(* Lors de l'evaluation d'un point fixe l'environnement est un pointeur *) (* sur la position correspondante a son code. *) -(* Dans le corps de chaque point fix le de Bruijn [nbr] represente, *) -(* le 1er point fix de la declaration mutuelle, le de Bruijn [1] le *) +(* Dans le corps de chaque point fixe le de Bruijn [nbr] represente, *) +(* le 1er point fixe de la declaration mutuelle, le de Bruijn [1] le *) (* nbr-ieme. *) (* L'acces a ces variables se fait par l'instruction [Koffsetclosure] *) (* (decalage de l'environnement) *) -(* Ceci permet de representer tout les point fix mutuels en un seul bloc *) -(* [Ct1 | ... | Ctn] est un tableau contant le code d'evaluation des *) +(* Ceci permet de representer les points fixes mutuels en un seul bloc *) +(* [Ct1 | ... | Ctn] est un tableau contenant le code d'evaluation des *) (* types des points fixes, ils sont utilises pour tester la conversion *) (* Leur environnement d'execution est celui du dernier point fix : *) (* [t1|C1| ... |tc|Cc| ... |t(nbr)|C(nbr)| fv1 | fv2 | .... | fvn | type] *) @@ -59,7 +73,7 @@ open Pre_env (* ... *) (* fcofixnbr = [clos_t | codenbr | a1 |...| anbr | fv1 |...| fvn | type] *) (* ^ *) -(* Les block [ai] sont des fonctions qui accumulent leurs arguments : *) +(* Les blocs [ai] sont des fonctions qui accumulent leurs arguments : *) (* ai arg1 argp ---> *) (* ai' = [A_t | accumulate | [Cfx_t | fcofixi] | arg1 | ... | argp ] *) (* Si un tel bloc arrive sur un [match] il faut forcer l'evaluation, *) @@ -68,10 +82,10 @@ open Pre_env (* l'evaluation : *) (* ai' <-- *) (* [A_t | accumulate | [Cfxe_t |fcofixi|result] | arg1 | ... | argp ] *) -(* L'avantage de cette representation est qu'elle permet d'evaluer qu'une *) -(* fois l'application d'un cofix (evaluation lazy) *) -(* De plus elle permet de creer facilement des cycles quand les cofix ne *) -(* n'ont pas d'aruments, ex: *) +(* L'avantage de cette representation est qu'elle permet de n'evaluer *) +(* qu'une fois l'application d'un cofix (evaluation lazy) *) +(* De plus elle permet de creer facilement des cycles quand les cofix *) +(* n'ont pas d'argument, ex: *) (* cofix one := cons 1 one *) (* a1 = [A_t | accumulate | [Cfx_t|fcofix1] ] *) (* fcofix1 = [clos_t | code | a1] *) diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 4a9c7da2b..962417c1e 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -1,3 +1,17 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $:Id:$ *) + +(* Author: Benjamin Grégoire as part of the bytecode-based virtual reduction + machine, Oct 2004 *) +(* Extension: Arnaud Spiwack (support for native arithmetic), May 2005 *) + open Names open Term open Cbytecodes diff --git a/kernel/closure.ml b/kernel/closure.ml index e77ea4cb3..86a42dc63 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -6,6 +6,19 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Created by Bruno Barras with Benjamin Werner's account to implement + a call-by-value conversion algorithm and a lazy reduction machine + with sharing, Nov 1996 *) +(* Addition of zeta-reduction (let-in contraction) by Hugo Herbelin, Oct 2000 *) +(* Call-by-value machine moved to cbv.ml, Mar 01 *) +(* Additional tools for module subtyping by Jacek Chrzaszcz, Aug 2002 *) +(* Extension with closure optimization by Bruno Barras, Aug 2003 *) +(* Support for evar reduction by Bruno Barras, Feb 2009 *) +(* Miscellaneous other improvements by Bruno Barras, 1997-2009 *) + +(* This file implements a lazy reduction for the Calculus of Inductive + Constructions *) + open Util open Pp open Term diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index 5e9db9c7d..edb03ecf5 100644 --- a/kernel/conv_oracle.ml +++ b/kernel/conv_oracle.ml @@ -6,6 +6,9 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Created by Bruno Barras as part of the rewriting of the conversion + algorithm, Nov 2001 *) + open Names (* Priority for the expansion of constant in the conversion test. diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 7b380944b..243efa795 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -6,6 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Created by Jean-Christophe Filliâtre out of V6.3 file constants.ml + as part of the rebuilding of Coq around a purely functional + abstract type-checker, Nov 1999 *) + +(* This module implements kernel-level discharching of local + declarations over global constants and inductive types *) + open Pp open Util open Names diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 145ca27d2..1c1645e97 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -1,3 +1,19 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +(* Created by Bruno Barras for Benjamin Grégoire as part of the + bytecode-based reduction machine, Oct 2004 *) +(* Bug fix #1419 by Jean-Marc Notin, Mar 2007 *) + +(* This file manages the table of global symbols for the bytecode machine *) + open Names open Term open Vm diff --git a/kernel/csymtable.mli b/kernel/csymtable.mli index 894a33ef5..160011f0b 100644 --- a/kernel/csymtable.mli +++ b/kernel/csymtable.mli @@ -1,3 +1,13 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + open Names open Term open Pre_env 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 = { diff --git a/kernel/environ.ml b/kernel/environ.ml index 69220908e..29374d24c 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -6,6 +6,20 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Author: Jean-Christophe Filliâtre as part of the rebuilding of Coq + around a purely functional abstract type-checker, Aug 1999 *) +(* Cleaning and lightening of the kernel by Bruno Barras, Nov 2001 *) +(* Flag for predicativity of Set by Hugo Herbelin in Oct 2003 *) +(* Support for virtual machine by Benjamin Grégoire in Oct 2004 *) +(* Support for retroknowledge by Arnaud Spiwack in May 2007 *) +(* Support for assumption dependencies by Arnaud Spiwack in May 2007 *) + +(* Miscellaneous maintenance by Bruno Barras, Hugo Herbelin, Jean-Marc + Notin, Matthieu Sozeau *) + +(* This file defines the type of environments on which the + type-checker works, together with simple related functions *) + open Util open Names open Sign diff --git a/kernel/esubst.ml b/kernel/esubst.ml index fd07d9297..04e0f507e 100644 --- a/kernel/esubst.ml +++ b/kernel/esubst.ml @@ -6,6 +6,10 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Created by Bruno Barras for Coq V7.0, Mar 2001 *) + +(* Support for explicit substitutions *) + open Util (*********************) diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 8abfe0943..c967bf1ba 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -6,6 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Created by Claudio Sacerdoti from contents of term.ml, names.ml and + new support for constant inlining in functor application, Nov 2004 *) +(* Optimizations and bug fixes by Élie Soubiran, from Feb 2008 *) + +(* This file provides types and functions for managing name + substitution in module constructions *) + open Pp open Util open Names diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index e67b987a6..b2e199ff8 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -6,6 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Created by Jacek Chrzaszcz, Aug 2002 as part of the implementation of + the Coq module system *) + +(* This module provides the main functions for type-checking module + declarations *) + open Util open Names open Univ diff --git a/kernel/modops.ml b/kernel/modops.ml index 084fdd4f4..38f59abe3 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -6,7 +6,15 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i*) +(* Created by Jacek Chrzaszcz, Aug 2002 as part of the implementation of + the Coq module system *) +(* Inlining and more liberal use of modules and module types by Claudio + Sacerdoti, Nov 2004 *) +(* New structure-based model of modules and miscellaneous bug fixes by + Élie Soubiran, from Feb 2008 *) + +(* This file provides with various operations on modules and module types *) + open Util open Pp open Names @@ -16,9 +24,6 @@ open Declarations open Environ open Entries open Mod_subst -(*i*) - - let error_existing_label l = error ("The label "^string_of_label l^" is already declared.") diff --git a/kernel/names.ml b/kernel/names.ml index 463f47ca4..d5f301f2f 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -6,6 +6,18 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* File created around Apr 1994 for CiC V5.10.5 by Chet Murthy collecting + parts of file initial.ml from CoC V4.8, Dec 1988, by Gérard Huet, + Thierry Coquand and Christine Paulin *) +(* Hash-consing by Bruno Barras in Feb 1998 *) +(* Extra functions for splitting/generation of identifiers by Hugo Herbelin *) +(* Restructuration by Jacek Chrzaszcz as part of the implementation of + the module system, Aug 2002 *) +(* Abstraction over the type of constant for module inlining by Claudio + Sacerdoti, Nov 2004 *) +(* Miscellaneous features or improvements by Hugo Herbelin, + Élie Soubiran, ... *) + open Pp open Util diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index 3835c81c5..d964ad1ba 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -6,6 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Created by Benjamin Grégoire out of environ.ml for better + modularity in the design of the bytecode virtual evaluation + machine, Dec 2005 *) +(* Bug fix by Jean-Marc Notin *) + +(* This file defines the type of kernel environments *) + open Util open Names open Sign diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 4a4661f99..e215f2336 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -6,6 +6,15 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Created under Benjamin Werner account by Bruno Barras to implement + a call-by-value conversion algorithm and a lazy reduction machine + with sharing, Nov 1996 *) +(* Addition of zeta-reduction (let-in contraction) by Hugo Herbelin, Oct 2000 *) +(* Irreversibility of opacity by Bruno Barras *) +(* Cleaning and lightening of the kernel by Bruno Barras, Nov 2001 *) +(* Equal inductive types by Jacek Chrzaszcz as part of the module + system, Aug 2002 *) + open Util open Names open Term diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml index c0f714f96..1dfafc08f 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -6,6 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Created by Arnaud Spiwack, May 2007 *) +(* Addition of native Head (nb of heading 0) and Tail (nb of trailing 0) by + Benjamin Grégoire, Jun 2007 *) + +(* This file defines the knowledge that the kernel is able to optimize + for evaluation in the bytecode virtual machine *) + open Term open Names diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index cffe7e772..6a18f72d5 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -6,6 +6,57 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Created by Jean-Christophe Filliâtre as part of the rebuilding of + Coq around a purely functional abstract type-checker, Dec 1999 *) + +(* This file provides the entry points to the kernel type-checker. It + defines the abstract type of well-formed environments and + implements the rules that build well-formed environments. + + An environment is made of constants and inductive types (E), of + section declarations (Delta), of local bound-by-index declarations + (Gamma) and of universe constraints (C). Below E[Delta,Gamma] |-_C + means that the tuple E, Delta, Gamma, C is a well-formed + environment. Main rules are: + + empty_environment: + + ------ + [,] |- + + push_named_assum(a,T): + + E[Delta,Gamma] |-_G + ------------------------ + E[Delta,Gamma,a:T] |-_G' + + push_named_def(a,t,T): + + E[Delta,Gamma] |-_G + --------------------------- + E[Delta,Gamma,a:=t:T] |-_G' + + add_constant(ConstantEntry(DefinitionEntry(c,t,T))): + + E[Delta,Gamma] |-_G + --------------------------- + E,c:=t:T[Delta,Gamma] |-_G' + + add_constant(ConstantEntry(ParameterEntry(c,T))): + + E[Delta,Gamma] |-_G + ------------------------ + E,c:T[Delta,Gamma] |-_G' + + add_mind(Ind(Ind[Gamma_p](Gamma_I:=Gamma_C))): + + E[Delta,Gamma] |-_G + ------------------------ + E,Ind[Gamma_p](Gamma_I:=Gamma_C)[Delta,Gamma] |-_G' + + etc. +*) + open Util open Names open Univ diff --git a/kernel/sign.ml b/kernel/sign.ml index f987a1f6c..43151d98c 100644 --- a/kernel/sign.ml +++ b/kernel/sign.ml @@ -6,6 +6,15 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Created by Jean-Christophe Filliâtre out of names.ml as part of the + rebuilding of Coq around a purely functional abstract type-checker, + Aug 1999 *) +(* Miscellaneous extensions, restructurations and bug-fixes by Hugo + Herbelin and Bruno Barras *) + +(* This file defines types and combinators regarding indexes-based and + names-based contexts *) + open Names open Util open Term diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 9bc719e7e..1b535ea43 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -6,6 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Created by Jacek Chrzaszcz, Aug 2002 as part of the implementation of + the Coq module system *) + +(* This module checks subtyping of module types *) + (*i*) open Util open Names @@ -20,8 +25,6 @@ open Mod_subst open Entries (*i*) - - (* This local type is used to subtype a constant with a constructor or an inductive type. It can also be useful to allow reorderings in inductive types *) diff --git a/kernel/term.ml b/kernel/term.ml index a1effb317..5f1c03188 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 diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index dac8ee47a..da3393065 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -6,6 +6,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +(* Created by Jacek Chrzaszcz, Aug 2002 as part of the implementation of + the Coq module system *) + +(* This module provides the main entry points for type-checking basic + declarations *) + open Util open Names open Univ diff --git a/kernel/univ.ml b/kernel/univ.ml index f42b6fb93..ca0d8fbd0 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -6,10 +6,13 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* Initial Caml version originates from CoC 4.8 [Dec 1988] *) -(* Extension with algebraic universes by HH [Sep 2001] *) +(* Created in Caml by Gérard Huet for CoC 4.8 [Dec 1988] *) +(* Functional code by Jean-Christophe Filliâtre for Coq V7.0 [1999] *) +(* Extension with algebraic universes by HH for Coq V7.0 [Sep 2001] *) (* Additional support for sort-polymorphic inductive types by HH [Mar 2006] *) +(* Revisions by Bruno Barras, Hugo Herbelin, Pierre Letouzey *) + (* Universes are stratified by a partial ordering $\le$. Let $\~{}$ be the associated equivalence. We also have a strict ordering $<$ between equivalence classes, and we maintain that $<$ is acyclic, diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index f2975d21c..cc064cd67 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 92968cad9..70241238d 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 32433f6be..df0f3e460 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 diff --git a/theories/Logic/Classical.v b/theories/Logic/Classical.v index 4a01f3fae..e75bfb4e6 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 afbb5e6df..f6c6446b4 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 45c487cf7..18ed260d4 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 ee6dd96f2..24544b908 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 14ab70b67..406429ffd 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 9c20905c7..d542ecdb1 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 d4d05fe1a..d10d6ff95 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 |