aboutsummaryrefslogtreecommitdiff
path: root/theories/Numbers/NatInt/NZSqrt.v
AgeCommit message (Expand)Author
2018-02-27Update headers following #6543.Théo Zimmermann
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-05-20Moving (e)transitivity out of the AST.Pierre-Marie Pédrot
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2012-08-08Updating headers.herbelin
2011-01-04f_equiv : a clone of f_equal that handles setoid equivalencesletouzey
2011-01-03Numbers: some improvements in proofsletouzey
2010-11-18NZSqrt: we define sqrt_up, a square root that rounds up instead of down as sqrtletouzey
2010-11-02NZSqrt : since spec is complete, no need for morphism axiom sqrt_wdletouzey
2010-11-02Numbers: misc improvementsletouzey
2010-11-02Numbers: specs about sqrt and pow of neg numbers, even in NZletouzey
2010-11-02Numbers: NZPowProp as a Module Type, some module variable renamingletouzey
2010-10-19Add sqrt in Numbersletouzey