aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2001-04-23Ajout Realsmayero
2001-04-23Ajouts Realsmayero
2001-04-23(One more) Minor layout adjustments for Library doccoq
2001-04-23Minor layout adjustments for Library doccoq
2001-04-20Ajout tactics Realsmayero
2001-04-20Library doc adjustments (until page 140)coq
2001-04-19typofilliatr
2001-04-19Ajout de fonctions proposees par Cuiht Alvaradomohring
2001-04-19BoolEq.v, une egalite generique a valeur dans boolmohring
2001-04-19remplace Zarith par ZArithmohring
2001-04-19remplace Zarith par ZArithmohring
2001-04-19Mise de (*i autour CVS infomohring
2001-04-19Mise de (*i autour CVS infomohring
2001-04-19Mise de (*i autour CVS infomohring
2001-04-19*** empty log message ***mohring
2001-04-19Remplacement Euclid_def Euclid_proof par Euclidmohring
2001-04-19Changement syntax pour Rinvmayero
2001-04-19Ajout de Fielddelahaye
2001-04-12Ajout de l'egalite de John Majormohring
2001-04-11coqwebfilliatr
2001-04-11documentation automatique de la bibliothèque standardfilliatr
2001-04-08Ajout lemmes arithmetiquesmohring
2001-04-08ajout des lemmes Zimmermanmohring
2001-03-30Ajout de lemmes sur les booleensmohring
2001-03-30Introduction d'une preuve de False_recmohring
2001-03-26Bibliotheque Nummohring
2001-03-15entetesfilliatr
2001-02-14Renommage des variables dans les schémas d'inductionherbelin
2001-02-08modif de la syntax: assoc a droite pour Ringmayero
2001-02-08simplification du make depend; fonctions de stat. util. memoire dans certains...filliatr
2001-02-01*** empty log message ***mohring
2001-02-01- coqc : option -imagefilliatr
2001-01-25Modif de l'axiomatisation pour enlever les /\ de _nemayero
2001-01-19Ajout d'un parseur d'entiers sous forme de patternherbelin
2001-01-15Essai d'axiomatisation des numeralmohring
2001-01-15Ajout de commentaire coqwebmohring
2001-01-11corr bug -mayero
2001-01-11Mise a jour Rbasemohring
2001-01-09Meta Definition -> Tactic Definitiondelahaye
2001-01-09Tactic Definition -> Meta Definitiondelahaye
2000-12-29Ajout du Let pour le langage de tactiquesdelahaye
2000-12-22*** empty log message ***mayero
2000-12-21Bug d'affichage à cause des << ... >>herbelin
2000-12-20Oublié de supprimer du code mortherbelin
2000-12-20Rétablissement de l'ancien comportement de Simpl sauf dans le cas mutuel ind...herbelin
2000-12-18Renommages autour de NewInductionherbelin
2000-12-15pb niveaumayero
2000-12-06Prise en compte `?' dans les `` ``herbelin
2000-12-05Reparation d'un bug de pretty-printdelahaye
2000-12-04caractere opaque des constantes repris en comptefilliatr
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 18:10:09 +0000