aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/mod_typing.ml
Commit message (Expand)AuthorAge
...
* cf. 12945Gravatar soubiran2010-04-16
* Variant !F M for functor application that does not honor the Inline declarationsGravatar letouzey2010-01-17
* Module type expressions of the form (Fsig X) with Definition foo := bar are n...Gravatar soubiran2009-10-28
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* retour sur le commit 11579 qui faisait plante les contribs FSet et color.Gravatar soubiran2008-11-14
* Les signatures des applications de foncteur sont précalculées, cela alourdi...Gravatar soubiran2008-11-12
* Correction bug 1979.Gravatar soubiran2008-10-28
* Correction bug #1969.Gravatar soubiran2008-10-21
* Report des commits 11417 et 11437 de la v8.2Gravatar soubiran2008-10-15
* Les contraintes d'univers sont maintenant collectées dans le champs mod_cons...Gravatar soubiran2008-06-25
* meilleur gestion de la fonction de "cache" des alias (declaremods), et correc...Gravatar soubiran2008-06-18
* correction bug 1839Gravatar soubiran2008-04-25
* correction d'un bug sur la compostion des substitutions induites par les alia...Gravatar soubiran2008-04-23
* correction bug 1839Gravatar soubiran2008-04-22
* fixed universes bug related to module inclusionGravatar barras2008-04-22
* Patch sur le typage d'un foncteur applique a un alias.Gravatar soubiran2008-04-03
* Correction de bugs relatifs a la compostion des substitutionsGravatar soubiran2008-03-25
* 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
* Removed some useless code in mod_typing that was redundant with safe_typing.Gravatar soubiran2007-02-21
* Fixed the pseudo-cicularity problem due to the with operator on Module Type.Gravatar soubiran2007-02-21
* modifications des messages d'erreurs renvoyés lors de la comparaison Gravatar soubiran2007-01-24
* Extension du polymorphisme de sorte au cas des définitions dans Type.Gravatar herbelin2006-10-28
* Changement des named_contextGravatar gregoire2005-12-02
* Construct "T with (Definition|Module) id := c" generalized toGravatar sacerdot2005-01-13
* HUGE COMMITGravatar sacerdot2005-01-03
* bug module with ... + vmGravatar barras2004-11-17
* Names.substitution (and related functions) and Term.subst_mps moved toGravatar sacerdot2004-11-16
* IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).Gravatar sacerdot2004-11-16
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* Nouvelle en-têteGravatar herbelin2004-07-16
* - fixed the Assert_failure error in kernel/modopsGravatar barras2004-02-18
* Bug 'with Module' corrigeGravatar coq2003-01-22
* Contexte locale non-vide interdit a la fin d'un module ou module typeGravatar coq2002-12-18
* Corrections de gestion des univers et modules + meilleure gestions des noms...Gravatar coq2002-12-09
* Lazy manuelles dans le codeGravatar coq2002-10-07
* Lazy experimentale temporaire...Gravatar coq2002-10-05
* La notation with dependante + affichage dependante de moduels corrigeGravatar coq2002-09-20
* La notation 'with'. L'interpretation - version preliminaireGravatar coq2002-08-19
* Strengthenning rules for modules + No modules in sectionsGravatar coq2002-08-16
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-26 16:01:15 +0000