aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2001-09-11Du bon usage des commentaires coqwebherbelin
2001-09-11Conformité des commentaires au format coqwebherbelin
2001-08-30Fin de la modif Exc/optionmohring
2001-08-29ajout option , Exc --> option, et lemmes dans les theoriesmohring
2001-08-13Rétablissement nom de section Map après résolution bugs surcharge de nomsherbelin
2001-08-13Protection des commentaires pour coqtex et coqwebherbelin
2001-08-05Expérimentation de NewDestruct et parfois NewInductionherbelin
2001-07-19modifs de preuves (plus simples)mayero
2001-07-16modif Map sectionmohring
2001-07-10Ajout du .v pour la tactique Setoid_replaceclrenard
2001-06-19Oubli Save + je sais plusmayero
2001-06-18Ajouts de lemmes (pour Float)mayero
2001-06-18Ajout du paradoxe de Berardi dans Logic (preuve que EM => PI dans CCI)barras
2001-06-04Correction bug outsidemayero
2001-05-31Creation du fichier Zhints.v repertoriant les thms de ZArith et definissant l...herbelin
2001-05-29Correction d'un bug du pretty-printclrenard
2001-05-15Modification pour passage p-automatesmohring
2001-05-07ex d'utilisation de fourier avec fieldmayero
2001-04-25coqwebfilliatr
2001-04-24correction nommayero
2001-04-24Ajout de Rseries et Rtrigo_funmayero
2001-04-24(Again) Little corrections for Library doccoq
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-24 13:08:13 +0000