aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/safe_typing.ml
Commit message (Expand)AuthorAge
* Moving printing of module typing errors upwards to himsg.ml so as toGravatar herbelin2011-03-05
* Mod_typing: some refactoring (common parts about MSEapply and co)Gravatar letouzey2011-02-11
* Safe_typing: some refactoring (avoiding copy-paste of record definitions)Gravatar letouzey2011-02-11
* A fine-grain control of inlining at functor application via priority levelsGravatar letouzey2011-01-31
* Univ.constraints made fully abstract instead of being a Set of abstract stuffGravatar letouzey2010-12-18
* Sharing is not anymore broken by traverse_module.Gravatar soubiran2010-09-15
* * kernel/Safe_typing.LightenLibrary:Gravatar regisgia2010-08-27
* * (checker|kernel)/Safe_typing:Gravatar regisgia2010-08-27
* * (checker|kernel)/Safe_typing:Gravatar regisgia2010-08-27
* * checker/SafeTyping kernel/SafeTyping:Gravatar regisgia2010-08-27
* * Improve documentation of LightenLibrary.Gravatar regisgia2010-08-27
* * (checker|kernel)/Safe_typing: New LightenLibrary.Gravatar regisgia2010-08-27
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Applicative commutative cuts in Fixpoint guard conditionGravatar pboutill2010-05-18
* Added a few informations about file lineages (for the most part in kernel)Gravatar herbelin2010-05-09
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Various bug fix on recent features of the module system:Gravatar soubiran2010-01-19
* 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
* Optionally list opaque constants in addition to axions/variables inGravatar msozeau2009-03-09
* Report des commits 11417 et 11437 de la v8.2Gravatar soubiran2008-10-15
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* Les contraintes d'univers sont maintenant collectées dans le champs mod_cons...Gravatar soubiran2008-06-25
* correction d'un bug sur la commande Include. Gravatar soubiran2008-06-10
* Ajout d'un comportement special du sous-typage pour les constantes opaques.Gravatar soubiran2008-06-09
* Correction du problème de complexité de Print Assumptions :Gravatar aspiwack2008-05-27
* fixed universes bug related to module inclusionGravatar barras2008-04-22
* Correction bug 1838 + doc modules.Gravatar soubiran2008-04-21
* Correction de bugs relatifs a la compostion des substitutionsGravatar soubiran2008-03-25
* Ajout des alias de module dans le noyau.Gravatar soubiran2008-03-14
* Patch bug #1799Gravatar soubiran2008-02-15
* Beaoucoup de changements dans la representation interne des modules.Gravatar soubiran2008-02-01
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
* Nettoyage de Print Assumptions :Gravatar aspiwack2007-11-09
* bug in safe_typing: univ constraints generated by section variables were not ...Gravatar barras2007-10-30
* 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
* Indentation + typoGravatar notin2006-09-01
* - Ajout d'un cast vm dans la syntaxe : x <: t Gravatar bgregoir2006-07-22
* Oh le joli bug dans le kernel:Gravatar letouzey2006-06-05
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
* 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
* bug #909: Top n'est cree que si le contexte est videGravatar barras2005-11-23
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
* Changement dans les boxed values .Gravatar gregoire2004-11-12
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* Nouvelle en-têteGravatar herbelin2004-07-16
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 15:38:47 +0000