aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals/Rtrigo_fun.v
Commit message (Expand)AuthorAge
* Réorganisation de la librairie des réelsGravatar desmettr2002-11-27
* Uniformisation (Qed/Save et Implicits Arguments)Gravatar herbelin2002-04-17
* Ajouts de lemmes (pour Float)Gravatar mayero2001-06-18
* Ajout de Rseries et Rtrigo_funGravatar mayero2001-04-24