aboutsummaryrefslogtreecommitdiff
path: root/library
AgeCommit message (Expand)Author
2003-03-29Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)herbelin
2003-03-26ajout d'une fonction reset_modmonate
2003-03-13Ajout réaffichage SubClassherbelin
2003-03-12*** empty log message ***barras
2003-02-24False dependencies in summarycoq
2003-02-05Ajout du traducteurdesmettr
2003-02-03release 7.4; changement magic numberfilliatr
2003-01-31Pour satisfaire ProofGeneralcoq
2003-01-27Deux p\'tits trucs ;)coq
2003-01-22Bug 'with Module' corrigecoq
2003-01-09Export M + Module M <: SIGcoq
2002-12-19Petit netoyage dans libcoq
2002-12-16Petit netoyage des open's et commentairescoq
2002-12-11Essai de hconsing local au declarationsherbelin
2002-12-10Hash-consing dès la lib_stkherbelin
2002-12-09Corrections de gestion des univers et modules + meilleure gestions des noms...coq
2002-12-05des Set et des Map en plusletouzey
2002-12-04Correction d'un message d'erreur de l'application de non-foncteurcoq
2002-12-02Ajout des options "Set Contextual Implicits" et "Set Strict Implicitsherbelin
2002-11-28Quelques Set et Map spécialisésletouzey
2002-11-26Affichage nom le plus court pour Syntactic Definitionherbelin
2002-11-24Ajout Refmapherbelin
2002-11-18Analyse plus fine des occurrences rigidesherbelin
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-11-08Correction bug PR#222coq
2002-11-05Intégration des modifs de la branche mowgli :herbelin
2002-10-29Préservation de la cohérence du cache en cas d'erreur au chargementherbelin
2002-10-29Prise en compte let-inherbelin
2002-10-28Des critères plus fins d'analyse des implicites automatiques; meilleur affic...herbelin
2002-10-12Nettoyageherbelin
2002-10-12Forcer la réouverture d'un fichier explicitement requis même si leherbelin
2002-10-10Nametab permet de definir le meme truc la deuxieme foiscoq
2002-09-27Encore quelques rangements dans Nametab + petits trucscoq
2002-09-24Un peu (plus) d'ordre dans Nametab...coq
2002-09-24Nametab data structure reorganisationcoq
2002-09-20La notation with dependante + affichage dependante de moduels corrigecoq
2002-08-19La notation 'with'. L'interpretation - version preliminairecoq
2002-08-19Pretty-printing preliminaire des modules, commandescoq
2002-08-17Suppression automatique du corps des définitions locales opaques dansherbelin
2002-08-16Strengthenning rules for modules + No modules in sectionscoq
2002-08-13Petites corrections ici et lacoq
2002-08-02Modules dans COQ\!\!\!\!coq
2002-06-03Protection des tactiques contre l'utilisation sans le bon contexte de thoriesherbelin
2002-06-03Protection des tactiques contre l'utilisation sans le bon contexte de thoriesherbelin
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2002-05-15MAJ V7.3herbelin
2002-04-16Déplacement/renommage de Class.stre_max en Declare.strength_minherbelin
2002-04-12Interdiction de nommer une constante comme une variable de section (plus simp...herbelin
2002-02-22suppression de pop_namedbarras
2002-02-14- Reforme de la gestion des args recursifs (via arbres reguliers)barras