aboutsummaryrefslogtreecommitdiff
path: root/theories/ZArith/Zsqrt_compat.v
AgeCommit message (Expand)Author
2019-07-26[stdlib] Remove deprecated module Zsqrt_compatVincent Laporte
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2018-02-27Update headers following #6543.Théo Zimmermann
2017-08-21Ensuring all .v files end with a newline to make "sed -i" work better on them.Hugo Herbelin
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2016-03-04Making parentheses mandatory in tactic scopes.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2013-11-02Restore Zsqrt compat now that refine works fine with match.aspiwack
2013-11-02A whole new implemenation of the refine tactic.aspiwack
2013-01-18Unset Asymmetric Patternspboutill
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
2011-06-28Deletion of useless Zsqrt_defletouzey
2011-05-05Modularization of BinInt, related fixes in the stdlibletouzey
2010-10-19Add sqrt in Numbersletouzey