aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/QArith/Qround.v
Commit message (Expand)AuthorAge
* Merge PR #6155: Get rid of ' notation for Zpos in QArithGravatar Maxime Dénès2018-03-09
|\
* | Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
| * Get rid of ' notation for Zpos in QArith.Gravatar Robbert Krebbers2017-11-14
|/
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Fix 3 unused-intro-pattern warnings in stdlib.Gravatar Théo Zimmermann2017-03-14
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* Updating headers.Gravatar herbelin2012-08-08
* Open Local Scope ---> Local Open Scope, same with Notation and aliiGravatar letouzey2012-07-05
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* Add small utility lemmas about nat/P/Z/Q arithmetic.Gravatar letouzey2010-11-02
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Implicit argument of Logic.eq become maximally insertedGravatar letouzey2009-10-08
* Reorganize Program and Classes theories. Requiring Setoid no longer setsGravatar msozeau2008-03-16
* Add Morphisms for Qceiling and QfloorGravatar roconnor2008-02-05
* Integration of theories/Ints/Z/* in ZArith and large cleanup and extension of...Gravatar letouzey2007-11-06
* Adding Qround.v (and helper lemmas and hints)Gravatar roconnor2007-11-01
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-21 17:50:31 +0000