aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
Commit message (Expand)AuthorAge
* Déplacement de Declare juste à la fin de interp pour pouvoir accéder à in...Gravatar herbelin2003-09-12
* Déplacement de Declare juste à la fin de interp pour pouvoir accéder à in...Gravatar herbelin2003-09-12
* errorGravatar herbelin2003-09-09
* Export process_module_bindings pour traducteurGravatar herbelin2003-09-02
* Nouvelle mouture du traducteur v7->v8Gravatar herbelin2003-08-11
* Passage des noms de tactiques à kernel_name pour compatibilité avec les fon...Gravatar herbelin2003-06-10
* Déplacement traducteur de nom dans Constrextern pour accès aux noms longsGravatar herbelin2003-06-10
* code mortGravatar herbelin2003-06-10
* Extension renommageGravatar herbelin2003-05-20
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
* CoqIde : but reset_modGravatar filliatr2003-05-19
* configure et make install s'occupent de CoqIde tout seulsGravatar filliatr2003-05-19
* but Require dans une SectionGravatar filliatr2003-05-19
* table des modules charges (Library.compunit_cache) synchronizee (pour CoqIde ...Gravatar filliatr2003-05-15
* Deplacement lemmes sur fact de Reals vers ArithGravatar herbelin2003-05-14
* Orthographe anglaise - typosGravatar herbelin2003-05-13
* Orthographe anglaiseGravatar herbelin2003-05-13
* Corrige Bug (PR#290)Gravatar coq2003-05-05
* En v8: abandon de Rle_sym2, Rle_sym1 au profit de Rge_le, Rle_ge; abandon de ...Gravatar herbelin2003-04-29
* simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = lis...Gravatar letouzey2003-04-16
* 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