coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Numbers: axiomatization, properties and implementations of gcd	letouzey	2010-11-05
*	Add small utility lemmas about nat/P/Z/Q arithmetic.	letouzey	2010-11-02
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
*	QArith: typo in name of hint db (fix #2346)	letouzey	2010-06-29
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
*	BigN, BigZ, BigQ: presentation via unique module with both ops and props	letouzey	2010-01-17
*	Avoid some more re-declarations of Equivalence instances	letouzey	2010-01-14
*	Nicer names: DecidableType2* --> Equalities, OrderedType2 --> Orders*	letouzey	2010-01-07
*	Rework of GenericMinMax: new axiomatic, split logical/decidable parts, Leibni...	letouzey	2010-01-07
*	OrderTac: use TotalOrder, no more "change" before calling "order" (stuff with...	letouzey	2010-01-07
*	Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...	letouzey	2009-12-09
*	No more specific syntax "Include Self" for inclusion of partially-applied fun...	letouzey	2009-12-07
*	Taking advantage of the new "Include Self Type" in DecidableType2 and NZAxioms	letouzey	2009-11-16
*	DecidableType: A specification via boolean equality as an alternative to eq_dec	letouzey	2009-11-10
*	Better visibility of the inductive CompSpec used to specify comparison functions	letouzey	2009-11-03
*	OrderedType implementation for various numerical datatypes + min/max structures	letouzey	2009-11-03
*	Remove various useless {struct} annotations	letouzey	2009-11-02
*	Implicit argument of Logic.eq become maximally inserted	letouzey	2009-10-08
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	changed deprecated setoid into relation	amahboub	2009-08-05
*	(Try to) use the conversion oracle also in w_unify to choose which constant to	msozeau	2008-10-03
*	Oups (on refait le 11268 en mieux)	herbelin	2008-07-27
*	- Pour CoRN, rétablissement notations Qgt/Qge (mais cette fois avec	herbelin	2008-07-26
*	Tauto breaking not only binary "conjunctions" seems like a bad idea	msozeau	2008-07-24
*	A try at allowing matching on applications as a binary syntax node by default.	msozeau	2008-07-22
*	Autour du parsing:	herbelin	2008-07-15
*	Fix bug #1899: no more strange notations for Qge and Qgt	letouzey	2008-07-04
*	- A little cleanup in Classes/*. Separate standard morphisms on	msozeau	2008-04-08
*	Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient	herbelin	2008-04-01
*	Reorganize Program and Classes theories. Requiring Setoid no longer sets	msozeau	2008-03-16
*	Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As part	msozeau	2008-03-07
*	Plug the new setoid implemtation in, leaving the original one commented	msozeau	2008-03-06
*	Add Morphisms for Qceiling and Qfloor	roconnor	2008-02-05
*	small improvements about Qc. Beware: Qlt_trans becomes Qclt_trans (as it ough...	letouzey	2007-11-24
*	small tactics "swap" and "absurd_hyp" are now obsolete: "contradict" is	letouzey	2007-11-06
*	Integration of theories/Ints/Z/* in ZArith and large cleanup and extension of...	letouzey	2007-11-06
*	Adding Qround.v (and helper lemmas and hints)	roconnor	2007-11-01
*	In agreement with Laurent Thery, start migration of auxiliary results	letouzey	2007-11-01
*	- renaming Qle_shift_recip_r into Qle_shift_inv_r, etc	roconnor	2007-09-07
*	Adding a few lemmas for reasoning about inequalities over the	roconnor	2007-08-28
*	Added Qpower_plus' and Zpower_Qpower	roconnor	2007-07-13
*	Small cleanup	letouzey	2007-07-13
*	Added Qpower_mult theorem.	roconnor	2007-07-05
*	Correction (partielle) du bug #1587	notin	2007-07-02
*	Updated Qpow_tac to work on a a more realistic set of exponent values.	roconnor	2007-06-25
*	Adding: Field instance for Q.	roconnor	2007-06-21
*	Changement dans le kernel :	bgregoir	2006-12-11
*	Mise en forme des theories	notin	2006-10-17
*	args implicites dans Field	barras	2006-09-29
*	separation de RealField	barras	2006-09-28