aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Reals/Rtrigo1.v
Commit message (Expand)AuthorAge
* Remove fourier pluginGravatar Maxime Dénès2018-07-17
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Simplify some proofs.Gravatar Guillaume Melquiond2017-04-02
* Make IZR a morphism for field.Gravatar Guillaume Melquiond2017-03-22
* Change the parser and printer so that they use IZR for real constants.Gravatar Guillaume Melquiond2017-03-22
* Make IZR use a compact representation of integers.Gravatar Guillaume Melquiond2017-03-22
* Simplify some proofs using ring and field.Gravatar Guillaume Melquiond2017-03-22
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* Make standard library independent of the names generated byGravatar Hugo Herbelin2014-06-04
* Making those proofs which depend on names generated for the argumentsGravatar Hugo Herbelin2014-06-01
* Remove some uses of excluded middle.Gravatar Guillaume Melquiond2014-04-22
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-16 03:51:12 +0000