aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
Commit message (Expand)AuthorAge
* Affichage forcé des implicites contextuels si pas de contexte connuGravatar herbelin2003-04-10
* Bug init_functionGravatar herbelin2003-04-09
* Synchronisation séparée des implicites pour l'affichage du traducteur;Gravatar herbelin2003-04-09
* Correction Show ImplicitsGravatar herbelin2003-04-09
* Gestion synchronisation des Impargs.*_out et des Impargs._strict dans ImpargsGravatar herbelin2003-04-09
* Synchronisation avec resetGravatar herbelin2003-04-09
* Réorganisation de Impargs + mise en place d'une infrastructureGravatar herbelin2003-04-09
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
* Renommage unicite/unicity pour la v8Gravatar herbelin2003-04-07
* Mise en place d'un traducteur de noms v7->v8Gravatar herbelin2003-03-31
* Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)Gravatar herbelin2003-03-29
* ajout d'une fonction reset_modGravatar monate2003-03-26
* Ajout réaffichage SubClassGravatar herbelin2003-03-13
* *** empty log message ***Gravatar barras2003-03-12
* False dependencies in summaryGravatar coq2003-02-24
* Ajout du traducteurGravatar desmettr2003-02-05
* release 7.4; changement magic numberGravatar filliatr2003-02-03
* Pour satisfaire ProofGeneralGravatar coq2003-01-31
* 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
* Essai de hconsing local au declarationsGravatar herbelin2002-12-11
* Hash-consing dès la lib_stkGravatar herbelin2002-12-10
* Corrections de gestion des univers et modules + meilleure gestions des noms...Gravatar coq2002-12-09
* des Set et des Map en plusGravatar letouzey2002-12-05
* Correction d'un message d'erreur de l'application de non-foncteurGravatar coq2002-12-04
* Ajout des options "Set Contextual Implicits" et "Set Strict ImplicitsGravatar herbelin2002-12-02
* Quelques Set et Map spécialisésGravatar letouzey2002-11-28
* Affichage nom le plus court pour Syntactic DefinitionGravatar herbelin2002-11-26
* Ajout RefmapGravatar herbelin2002-11-24
* Analyse plus fine des occurrences rigidesGravatar herbelin2002-11-18
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Correction bug PR#222Gravatar coq2002-11-08
* Intégration des modifs de la branche mowgli :Gravatar herbelin2002-11-05
* Préservation de la cohérence du cache en cas d'erreur au chargementGravatar herbelin2002-10-29
* Prise en compte let-inGravatar herbelin2002-10-29
* Des critères plus fins d'analyse des implicites automatiques; meilleur affic...Gravatar herbelin2002-10-28
* NettoyageGravatar herbelin2002-10-12
* Forcer la réouverture d'un fichier explicitement requis même si leGravatar herbelin2002-10-12
* Nametab permet de definir le meme truc la deuxieme foisGravatar coq2002-10-10
* Encore quelques rangements dans Nametab + petits trucsGravatar coq2002-09-27
* Un peu (plus) d'ordre dans Nametab...Gravatar coq2002-09-24
* Nametab data structure reorganisationGravatar coq2002-09-24
* La notation with dependante + affichage dependante de moduels corrigeGravatar coq2002-09-20
* La notation 'with'. L'interpretation - version preliminaireGravatar coq2002-08-19
* Pretty-printing preliminaire des modules, commandesGravatar coq2002-08-19
* Suppression automatique du corps des définitions locales opaques dansGravatar herbelin2002-08-17
* Strengthenning rules for modules + No modules in sectionsGravatar coq2002-08-16