aboutsummaryrefslogtreecommitdiff
path: root/theories/QArith/Qround.v
AgeCommit message (Expand)Author
2018-03-09Merge PR #6155: Get rid of ' notation for Zpos in QArithMaxime Dénès
2018-02-27Update headers following #6543.Théo Zimmermann
2017-11-14Get rid of ' notation for Zpos in QArith.Robbert Krebbers
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-03-14Fix 3 unused-intro-pattern warnings in stdlib.Théo Zimmermann
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2012-08-08Updating headers.herbelin
2012-07-05Open Local Scope ---> Local Open Scope, same with Notation and aliiletouzey
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
2010-11-02Add small utility lemmas about nat/P/Z/Q arithmetic.letouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2009-10-08Implicit argument of Logic.eq become maximally insertedletouzey
2008-03-16Reorganize Program and Classes theories. Requiring Setoid no longer setsmsozeau
2008-02-05Add Morphisms for Qceiling and Qfloorroconnor
2007-11-06Integration of theories/Ints/Z/* in ZArith and large cleanup and extension of...letouzey
2007-11-01Adding Qround.v (and helper lemmas and hints)roconnor
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 05:17:00 +0000