aboutsummaryrefslogtreecommitdiff
path: root/theories/Reals/Rbase.v
AgeCommit message (Expand)Author
2001-08-05Expérimentation de NewDestruct et parfois NewInductionherbelin
2001-06-19Oubli Save + je sais plusmayero
2001-06-18Ajouts de lemmes (pour Float)mayero
2001-04-23Ajouts Realsmayero
2001-04-23Minor layout adjustments for Library doccoq
2001-04-20Ajout tactics Realsmayero
2001-04-20Library doc adjustments (until page 140)coq
2001-04-19Changement syntax pour Rinvmayero
2001-04-19Ajout de Fielddelahaye
2001-03-15entetesfilliatr
2001-02-14Renommage des variables dans les schémas d'inductionherbelin
2001-01-25Modif de l'axiomatisation pour enlever les /\ de _nemayero
2001-01-11Mise a jour Rbasemohring
2000-11-23Ajout d'une syntaxe pour Reals.mayero
2000-11-10mise-a-jour, ajouts de quelques truc...mayero
2000-11-05Pour ne plus éviter temporairement le "Auto with zarith" !herbelin
2000-10-30Pour eviter temporairement le "Auto with zarith"delahaye
2000-06-21theories/Realsfilliatr