aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Zarith
Commit message (Expand)AuthorAge
* Renommage des variables dans les schémas d'inductionGravatar herbelin2001-02-14
* simplification du make depend; fonctions de stat. util. memoire dans certains...Gravatar filliatr2001-02-08
* - coqc : option -imageGravatar filliatr2001-02-01
* Ajout de commentaire coqwebGravatar mohring2001-01-15
* Mise a jour RbaseGravatar mohring2001-01-11
* Meta Definition -> Tactic DefinitionGravatar delahaye2001-01-09
* Tactic Definition -> Meta DefinitionGravatar delahaye2001-01-09
* Rétablissement de l'ancien comportement de Simpl sauf dans le cas mutuel ind...Gravatar herbelin2000-12-20
* Elimination du 'Gravatar delahaye2000-11-28
* Remettre une section dans fast_integer pour contourner un bug de définition ...Gravatar herbelin2000-11-27
* Nettoyage + prise en compte noms longsGravatar herbelin2000-11-20
* Suppression de la section fast_integer qui cachait le nom du module éponymeGravatar herbelin2000-11-20
* Y avait des '.' non suivis d'un séparateurGravatar herbelin2000-11-11
* Passage command -> constrGravatar herbelin2000-10-27
* g_natsyntax et g_zsyntax maintenant toujours linkesGravatar filliatr2000-10-27
* Parsing des motifs de Syntax avec la grammaire associée à l'univers de la d...Gravatar herbelin2000-10-18
* Finalement, encore un Simpl inutileGravatar herbelin2000-10-10
* Changement dans la stratégie de réduction du Fix par SimplGravatar herbelin2000-10-06
* Ajout du langage de tactiquesGravatar delahaye2000-05-03
* portage Omega (mais toujours pas Zpower et Zlogarithm)Gravatar filliatr2000-05-02
* suppression doublonGravatar filliatr2000-04-26
* erreurs lexicales dans les patterns (manquait des espaces)Gravatar filliatr2000-03-30
* - bug make_module_marker (plus de # et de .obj maintenant)Gravatar filliatr2000-03-21
* Retour sur les anciens nomsGravatar herbelin2000-03-21
* ZarithGravatar filliatr2000-03-18
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-16 21:28:37 +0000