aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/ZArith/Zsqrt_compat.v
Commit message (Expand)AuthorAge
* 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