aboutsummaryrefslogtreecommitdiff
path: root/theories/Reals/Rsyntax.v
AgeCommit message (Expand)Author
2002-06-06Correction non reconnaissance des variables de section dans les afficheurs de...herbelin
2002-05-29Double Induction prend maintenant des noms d'hyppthèsesherbelin
2002-03-22Bug d'affichage des réels dû à une collision entre les APPLINSIDETAIL de Z...herbelin
2001-12-04Backtrack sur le commit du 30.11.2001delahaye
2001-11-30*** empty log message ***desmettr
2001-10-23Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrRdelahaye
2001-09-11Un look un peu plus avenant aux productions des règles de grammaireherbelin
2001-07-19modifs de preuves (plus simples)mayero
2001-06-04Correction bug outsidemayero
2001-04-24Ajout de Rseries et Rtrigo_funmayero
2001-04-20Library doc adjustments (until page 140)coq
2001-04-19Mise de (*i autour CVS infomohring
2001-04-19Changement syntax pour Rinvmayero
2001-03-15entetesfilliatr
2001-02-08modif de la syntax: assoc a droite pour Ringmayero
2001-01-11corr bug -mayero
2000-12-22*** empty log message ***mayero
2000-12-15pb niveaumayero
2000-12-06Prise en compte `?' dans les `` ``herbelin
2000-12-05Reparation d'un bug de pretty-printdelahaye
2000-11-23Ajout d'une syntaxe pour Reals.mayero
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-19 15:13:21 +0000