coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Merge PR #6155: Get rid of ' notation for Zpos in QArith	Maxime Dénès	2018-03-09
\|\
* \|	Update headers following #6543.	Théo Zimmermann	2018-02-27
\| \|
\| *	Get rid of ' notation for Zpos in QArith.	Robbert Krebbers	2017-11-14
\|/
*	Add Qabs_Qinv: Qabs (/ q) == / (Qabs q).	Raphaël Monat	2017-10-03
\|
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\|
*	Update copyright headers.	Maxime Dénès	2016-01-20
\|
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	Updating headers.	herbelin	2012-08-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ZArith + other : favor the use of modern names instead of compat notations	letouzey	2012-07-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- For instance, refl_equal --> eq_refl - Npos, Zpos, Zneg now admit more uniform qualified aliases N.pos, Z.pos, Z.neg. - A new module BinInt.Pos2Z with results about injections from positive to Z - A result about Z.pow pushed in the generic layer - Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l} - Using tactic Z.le_elim instead of Zle_lt_or_eq - Some cleanup in ring, field, micromega (use of "Equivalence", "Proper" ...) - Some adaptions in QArith (for instance changed Qpower.Qpower_decomp) - In ZMake and ZMake, functor parameters are now named NN and ZZ instead of N and Z for avoiding confusions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15515 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add small utility lemmas about nat/P/Z/Q arithmetic.	letouzey	2010-11-02
\| \| \| \| \| \|	Initial patch by Eelis van der Weegen, minor adaptations by myself git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13613 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Add Morphisms for Qceiling and Qfloor	roconnor	2008-02-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10508 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- renaming Qle_shift_recip_r into Qle_shift_inv_r, etc	roconnor	2007-09-07
\| \| \| \| \| \| \| \| \| \| \| \|	- Adding Qlt_shift_div_l, etc - Adding Qabs_Qmult : forall a b, Qabs (ab) == (Qabs a)(Qabs b). - Adding Qle_Qabs : forall a, a <= Qabs a. - Removing redudnent Qminus' x y := Qred (Qminus x y) from Qabs. It is already defined elsewhere (in it's proper place). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10118 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Adding: Field instance for Q.	roconnor	2007-06-21
	: Power function from Q -> Z -> Q. : Absolute value function. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9901 85f007b7-540e-0410-9357-904b9bb8a0f7