index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
library
/
declaremods.ml
Commit message (
Expand
)
Author
Age
*
Enhancements to coqdoc, better globalization of sections and modules.
msozeau
2008-06-06
*
ajout d'un printer pour les contraintes d'univers + correction d'un bug sur l...
soubiran
2008-06-06
*
** Efficacité, bugs, robustesse CoqIDE **
herbelin
2008-05-08
*
correction bug 1839
soubiran
2008-04-25
*
correction d'un bug sur la compostion des substitutions induites par les alia...
soubiran
2008-04-23
*
correction bug 1839
soubiran
2008-04-22
*
corection bug #1837
soubiran
2008-04-21
*
Correction bug 1838 + doc modules.
soubiran
2008-04-21
*
Correction bug 1818, 3eme commentaire. mauvaise generation de substitution a ...
soubiran
2008-04-03
*
Correction d'un bug sur Import/Export : ces fonctionnalites sont gerees en-de...
soubiran
2008-03-26
*
Correction de bugs relatifs a la compostion des substitutions
soubiran
2008-03-25
*
Correction d'un bug sur les modules de la forme:
soubiran
2008-03-20
*
Ajout des alias de module dans le noyau.
soubiran
2008-03-14
*
Correction d'un bug sur les substitutions:
soubiran
2008-02-05
*
declaremods.ml
soubiran
2008-02-04
*
Beaoucoup de changements dans la representation interne des modules.
soubiran
2008-02-01
*
Commit intermédiaire express de réparation de coqide.ml, que j'avais
aspiwack
2007-12-06
*
Factorisation des opérations sur le type option de Util dans un module
aspiwack
2007-12-05
*
Removed some useless code in mod_typing that was redundant with safe_typing.
soubiran
2007-02-21
*
Correction bug #1364 (les variables de section sont repérées par
herbelin
2007-02-07
*
Standardisation nom option_app en option_map
herbelin
2006-04-27
*
Nouveau mécanisme pour les modules interactifs : les arguments de
herbelin
2006-04-16
*
Inversion de l'ordre de chargement des objets logiques et non logiques
herbelin
2006-04-15
*
Tentative de réparation du bug #1025: it seems like that a casted module sho...
herbelin
2005-12-24
*
Nettoyage suite à la détection par défaut des variables inutilisées par o...
herbelin
2005-11-08
*
Keep ClosedSection marker for reset
herbelin
2005-02-20
*
Code mort
herbelin
2005-02-18
*
Construct "T with (Definition|Module) id := c" generalized to
sacerdot
2005-01-13
*
- Module/Declare Module syntax made more uniform:
sacerdot
2005-01-06
*
HUGE COMMIT
sacerdot
2005-01-03
*
Names.substitution (and related functions) and Term.subst_mps moved to
sacerdot
2004-11-16
*
Nouvelle en-tête
herbelin
2004-07-16
*
meilleure presentation des commentaires du traducteur
barras
2004-01-02
*
Correction du bug 335 et Export/Require Export dans un module
coq
2003-10-07
*
Corrige Bug (PR#290)
coq
2003-05-05
*
Deux p\'tits trucs ;)
coq
2003-01-27
*
Bug 'with Module' corrige
coq
2003-01-22
*
Export M + Module M <: SIG
coq
2003-01-09
*
Petit netoyage dans lib
coq
2002-12-19
*
Petit netoyage des open's et commentaires
coq
2002-12-16
*
Corrections de gestion des univers et modules + meilleure gestions des noms...
coq
2002-12-09
*
Correction d'un message d'erreur de l'application de non-foncteur
coq
2002-12-04
*
Correction bug PR#222
coq
2002-11-08
*
Encore quelques rangements dans Nametab + petits trucs
coq
2002-09-27
*
La notation with dependante + affichage dependante de moduels corrige
coq
2002-09-20
*
La notation 'with'. L'interpretation - version preliminaire
coq
2002-08-19
*
Strengthenning rules for modules + No modules in sections
coq
2002-08-16
*
Petites corrections ici et la
coq
2002-08-13
*
Modules dans COQ\!\!\!\!
coq
2002-08-02