aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/ZArith/Zsqrt_compat.v
Commit message (Expand)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Ensuring all .v files end with a newline to make "sed -i" work better on them.Gravatar Hugo Herbelin2017-08-21
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Making parentheses mandatory in tactic scopes.Gravatar Pierre-Marie Pédrot2016-03-04
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* Restore Zsqrt compat now that refine works fine with match.Gravatar aspiwack2013-11-02
* A whole new implemenation of the refine tactic.Gravatar aspiwack2013-11-02
* Unset Asymmetric PatternsGravatar pboutill2013-01-18
* 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
* Deletion of useless Zsqrt_defGravatar letouzey2011-06-28
* Modularization of BinInt, related fixes in the stdlibGravatar letouzey2011-05-05
* Add sqrt in NumbersGravatar letouzey2010-10-19
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-21 01:50:53 +0000