aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/ZArith/Zpow_facts.v
Commit message (Expand)AuthorAge
* Zpow_facts.Zmult_power: kills a useless hypothesisGravatar letouzey2008-06-11
* Cyclic31: migrate auxiliary lemmas to their legitimate filesGravatar letouzey2008-05-27
* Backtrack on using metas eagerly in auto, only done in "new auto" forGravatar msozeau2008-04-28
* - Fix bug in unification not taking into account the right metaGravatar msozeau2008-04-27
* Keep the Z_scope local to this file.Gravatar roconnor2008-01-24
* small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is Gravatar letouzey2007-11-06
* Integration of theories/Ints/Z/* in ZArith and large cleanup and extension of...Gravatar letouzey2007-11-06