coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	micromega : vm_compute; reflexivity -> vm_cast_no_check (eq_refl true)	Frédéric Besson	2014-08-01
\| \| \| \|	* Thanks to G. Melquiond for pointing out that 'abstract' already performs type-checking
*	micromega : improve efficiency/termination of type-checking	Frédéric Besson	2014-08-01
\| \| \| \| \|	* unused terms are generalised * proof is abstract
*	micromega : refification recognises @eq T for T convertible with Z or R	Frédéric Besson	2014-07-31
\|
*	micromega: removal of spurious Export; addition of Lia.v encapsulating lia ↵	Frédéric Besson	2013-12-20
\| \| \| \|	and nia.
*	Updating headers.	herbelin	2012-08-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Legacy Ring and Legacy Field migrated to contribs	letouzey	2012-07-05
\| \| \| \| \| \| \| \| \|	One slight point to check someday : fourier used to launch a tactic called Ring.polynom in some cases. It it crucial ? If so, how to replace with the setoid_ring equivalent ? git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15524 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
*	update of Micromega doc	fbesson	2011-06-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14248 85f007b7-540e-0410-9357-904b9bb8a0f7
*	improved tactic names	fbesson	2011-06-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14242 85f007b7-540e-0410-9357-904b9bb8a0f7
*	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14152 ↵	fbesson	2011-05-23
\| \| \| \|	85f007b7-540e-0410-9357-904b9bb8a0f7
*	added support to handle division by a constant over R	fbesson	2011-05-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14147 85f007b7-540e-0410-9357-904b9bb8a0f7
*	cbv delta - [...] before calling lia	fbesson	2011-05-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14140 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Improved lia + experimental nlia	fbesson	2011-05-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14116 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
*	Application des patches envoyés par F. Besson pour micromega	notin	2010-03-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12852 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
*	micromega : Better parsing of formulae - smaller proof terms for Z - ↵	fbesson	2009-07-30
\| \| \| \| \| \|	redesign of proof cache git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12254 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ↵	letouzey	2009-03-20
	user contribs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11996 85f007b7-540e-0410-9357-904b9bb8a0f7