aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/ZArith/ZArith_dec.v
Commit message (Expand)AuthorAge
* Ajout Open ScopeGravatar herbelin2003-04-09
* Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import".Gravatar herbelin2003-04-09
* *** empty log message ***Gravatar barras2003-03-12
* Making the sumbool functions transparent, so that they can used toGravatar bertot2002-07-09
* Adding file theories/ZArith/Zsqrt.v that contains a square root function.Gravatar bertot2002-06-07
* suppression de inf_decidable dans ZArith_dec (pour SeachPattern)Gravatar filliatr2002-05-16
* Uniformisation (Qed/Save et Implicits Arguments)Gravatar herbelin2002-04-17
* remplace Zarith par ZArithGravatar mohring2001-04-19