aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/declaremods.ml
Commit message (Expand)AuthorAge
* Correction bug 1818, 3eme commentaire. mauvaise generation de substitution a ...Gravatar soubiran2008-04-03
* Correction d'un bug sur Import/Export : ces fonctionnalites sont gerees en-de...Gravatar soubiran2008-03-26
* Correction de bugs relatifs a la compostion des substitutionsGravatar soubiran2008-03-25
* Correction d'un bug sur les modules de la forme:Gravatar soubiran2008-03-20
* Ajout des alias de module dans le noyau.Gravatar soubiran2008-03-14
* Correction d'un bug sur les substitutions:Gravatar soubiran2008-02-05
* declaremods.mlGravatar soubiran2008-02-04
* Beaoucoup de changements dans la representation interne des modules.Gravatar soubiran2008-02-01
* Commit intermédiaire express de réparation de coqide.ml, que j'avais Gravatar aspiwack2007-12-06
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
* Removed some useless code in mod_typing that was redundant with safe_typing.Gravatar soubiran2007-02-21
* Correction bug #1364 (les variables de section sont repérées parGravatar herbelin2007-02-07
* 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
* Tentative de réparation du bug #1025: it seems like that a casted module sho...Gravatar herbelin2005-12-24
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* Keep ClosedSection marker for resetGravatar herbelin2005-02-20
* Code mortGravatar herbelin2005-02-18
* Construct "T with (Definition|Module) id := c" generalized toGravatar sacerdot2005-01-13
* - Module/Declare Module syntax made more uniform:Gravatar sacerdot2005-01-06
* HUGE COMMITGravatar sacerdot2005-01-03
* Names.substitution (and related functions) and Term.subst_mps moved toGravatar sacerdot2004-11-16
* Nouvelle en-têteGravatar herbelin2004-07-16
* meilleure presentation des commentaires du traducteurGravatar barras2004-01-02
* Correction du bug 335 et Export/Require Export dans un moduleGravatar coq2003-10-07
* Corrige Bug (PR#290)Gravatar coq2003-05-05
* Deux p\'tits trucs ;)Gravatar coq2003-01-27
* Bug 'with Module' corrigeGravatar coq2003-01-22
* Export M + Module M <: SIGGravatar coq2003-01-09
* Petit netoyage dans libGravatar coq2002-12-19
* Petit netoyage des open's et commentairesGravatar coq2002-12-16
* Corrections de gestion des univers et modules + meilleure gestions des noms...Gravatar coq2002-12-09
* Correction d'un message d'erreur de l'application de non-foncteurGravatar coq2002-12-04
* Correction bug PR#222Gravatar coq2002-11-08
* Encore quelques rangements dans Nametab + petits trucsGravatar coq2002-09-27
* 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
* Petites corrections ici et laGravatar coq2002-08-13
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02