aboutsummaryrefslogtreecommitdiff
path: root/theories/Reals/Rtrigo1.v
AgeCommit message (Expand)Author
2013-12-03Fix statement of Rplus_lt_reg_r and add Rplus_lt_reg_l.Guillaume Melquiond
2012-08-08Updating headers.herbelin
2012-07-05Some cleanup in recent proofs concerning piletouzey
2012-06-11These files are displaced from Rtrigo.v and Ranalysis_reg.vbertot