aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/global.ml
Commit message (Expand)AuthorAge
* Conv_orable made functional and part of pre_envGravatar gareuselesinge2013-10-31
* Future: ported to Ephemeron + exception enhancingGravatar gareuselesinge2013-10-18
* Safe_typing code refactoringGravatar letouzey2013-08-20
* enhance marshallable option for freeze (minor TODO in safe_typing)Gravatar gareuselesinge2013-08-08
* Simple machinery to detect EXTEND that interpret during parsingGravatar gareuselesinge2013-08-08
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Added a Register Inline command for the native compiler. Will be ported to th...Gravatar mdenes2013-07-10
* code simplifications concerning SummaryGravatar letouzey2013-04-22
* Minor simplifications in Declaremods and Safe_typingGravatar letouzey2013-04-15
* Mod_subst: misc reformulationsGravatar letouzey2013-02-26
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
* Modulification of LabelGravatar ppedrot2012-12-18
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* Partial revert of Yann commit in order to use CLib.List when openingGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* Module names and constant/inductive names are now in two separate namespacesGravatar letouzey2012-03-26
* Noise for nothingGravatar pboutill2012-03-02
* Various simplifications about constant_of_delta and mind_of_deltaGravatar letouzey2011-10-11
* Rely on kernel to know if a name is already used so as to be consistent with it.Gravatar herbelin2011-10-08
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Variant !F M for functor application that does not honor the Inline declarationsGravatar letouzey2010-01-17
* Include Self (Type) Foo: applying a (Type) Functor to the current contextGravatar letouzey2009-11-16
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Death of "survive_module" and "survive_section" (the first one wasGravatar herbelin2009-08-13
* Ajout des alias de module dans le noyau.Gravatar soubiran2008-03-14
* Beaoucoup de changements dans la representation interne des modules.Gravatar soubiran2008-02-01
* Processor integers + Print assumption (see coqdev mailing list for the Gravatar aspiwack2007-05-11
* Extension du polymorphisme de sorte au cas des définitions dans Type.Gravatar herbelin2006-10-28
* Nouveau mécanisme pour les modules interactifs : les arguments deGravatar herbelin2006-04-16
* Inversion de l'ordre de chargement des objets logiques et non logiquesGravatar herbelin2006-04-15
* Changement des named_contextGravatar gregoire2005-12-02
* bug #909: Top n'est cree que si le contexte est videGravatar barras2005-11-23
* Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changedGravatar sacerdot2005-01-14
* dead (and obsolete) code (in comments) removedGravatar sacerdot2004-11-16
* Nouvelle en-têteGravatar herbelin2004-07-16
* Options -strongly-constructive et -strongly-classicalGravatar herbelin2003-10-28
* Correction du bug 335 et Export/Require Export dans un moduleGravatar coq2003-10-07
* Corrections de gestion des univers et modules + meilleure gestions des noms...Gravatar coq2002-12-09
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* suppression de pop_namedGravatar barras2002-02-22
* Fusion de declare/add_constant, declare/add_parameter et add_discharged_constantGravatar herbelin2001-11-20
* Déplacement et export de type_of_global dans GlobalGravatar herbelin2001-11-09
* GROS COMMIT:Gravatar barras2001-11-05
* Abstraction de l'immplementation de dirpath et implementation dans l'autre se...Gravatar herbelin2001-10-17
* TransparentGravatar barras2001-09-20
* Mécanisme pour faire remonter les contraintes de typage sur les variables de...Gravatar herbelin2001-09-09