aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals/Rtrigo1.v
Commit message (Expand)AuthorAge
* Fix statement of Rplus_lt_reg_r and add Rplus_lt_reg_l.Gravatar Guillaume Melquiond2013-12-03
* Updating headers.Gravatar herbelin2012-08-08
* Some cleanup in recent proofs concerning piGravatar letouzey2012-07-05
* These files are displaced from Rtrigo.v and Ranalysis_reg.vGravatar bertot2012-06-11