coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Cleanup of files related with power over Z.	letouzey	2011-07-01
	- Zpow_def, Zpower, Zpow_facts shortened thanks to stuff in BinInt.Z - The alternative Zpower_alt is now in a separate file Zpow_alt.v, not loaded by default. - Some more injection lemmas in Znat (pow, div, mod, quot, rem) - Btw, added a "square" function in Z, N, Pos, ... (instead of Zpow_facts.Zsquare). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14253 85f007b7-540e-0410-9357-904b9bb8a0f7