index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
kernel
/
mod_typing.ml
Age
Commit message (
Expand
)
Author
2010-01-17
Variant !F M for functor application that does not honor the Inline declarations
letouzey
2009-10-28
Module type expressions of the form (Fsig X) with Definition foo := bar are n...
soubiran
2009-10-21
This big commit addresses two problems:
soubiran
2009-09-17
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2008-11-14
retour sur le commit 11579 qui faisait plante les contribs FSet et color.
soubiran
2008-11-12
Les signatures des applications de foncteur sont précalculées, cela alourdi...
soubiran
2008-10-28
Correction bug 1979.
soubiran
2008-10-21
Correction bug #1969.
soubiran
2008-10-15
Report des commits 11417 et 11437 de la v8.2
soubiran
2008-06-25
Les contraintes d'univers sont maintenant collectées dans le champs mod_cons...
soubiran
2008-06-18
meilleur gestion de la fonction de "cache" des alias (declaremods), et correc...
soubiran
2008-04-25
correction bug 1839
soubiran
2008-04-23
correction d'un bug sur la compostion des substitutions induites par les alia...
soubiran
2008-04-22
correction bug 1839
soubiran
2008-04-22
fixed universes bug related to module inclusion
barras
2008-04-03
Patch sur le typage d'un foncteur applique a un alias.
soubiran
2008-03-25
Correction de bugs relatifs a la compostion des substitutions
soubiran
2008-03-14
Ajout des alias de module dans le noyau.
soubiran
2008-02-01
Beaoucoup de changements dans la representation interne des modules.
soubiran
2007-05-11
Processor integers + Print assumption (see coqdev mailing list for the
aspiwack
2007-02-21
Removed some useless code in mod_typing that was redundant with safe_typing.
soubiran
2007-02-21
Fixed the pseudo-cicularity problem due to the with operator on Module Type.
soubiran
2007-01-24
modifications des messages d'erreurs renvoyés lors de la comparaison
soubiran
2006-10-28
Extension du polymorphisme de sorte au cas des définitions dans Type.
herbelin
2005-12-02
Changement des named_context
gregoire
2005-01-13
Construct "T with (Definition|Module) id := c" generalized to
sacerdot
2005-01-03
HUGE COMMIT
sacerdot
2004-11-17
bug module with ... + vm
barras
2004-11-16
Names.substitution (and related functions) and Term.subst_mps moved to
sacerdot
2004-11-16
IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).
sacerdot
2004-10-20
COMMITED BYTECODE COMPILER
barras
2004-07-16
Nouvelle en-tête
herbelin
2004-02-18
- fixed the Assert_failure error in kernel/modops
barras
2003-01-22
Bug 'with Module' corrige
coq
2002-12-18
Contexte locale non-vide interdit a la fin d'un module ou module type
coq
2002-12-09
Corrections de gestion des univers et modules + meilleure gestions des noms...
coq
2002-10-07
Lazy manuelles dans le code
coq
2002-10-05
Lazy experimentale temporaire...
coq
2002-09-20
La notation with dependante + affichage dependante de moduels corrige
coq
2002-08-19
La notation 'with'. L'interpretation - version preliminaire
coq
2002-08-16
Strengthenning rules for modules + No modules in sections
coq
2002-08-02
Modules dans COQ\!\!\!\!
coq