aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/ZArith/Zpow_facts.v
Commit message (Expand)AuthorAge
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* Simpl less (so that cbn will not simpl too much)Gravatar Pierre Boutillier2014-10-01
* Updating headers.Gravatar herbelin2012-08-08
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* Notation: a new annotation "compat 8.x" extending "only parsing"Gravatar letouzey2012-07-05
* Cleanup of files related with power over Z.Gravatar letouzey2011-07-01
* Modularization of BinInt, related fixes in the stdlibGravatar letouzey2011-05-05
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Remove various useless {struct} annotationsGravatar letouzey2009-11-02
* Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'Gravatar letouzey2009-10-08
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-22 09:06:35 +0000