coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Add some missing Proof statements.	Guillaume Melquiond	2014-09-17
*	Fixing bug #3270. Patch by Robbert Krebbers.	Pierre-Marie Pédrot	2014-07-08
*	Revert "Fix Qcanon after changes on injection."	Maxime Dénès	2014-05-18
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Eta contractions to please cbn	Pierre Boutillier	2014-05-02
*	Fix Qcanon after changes on injection.	Maxime Dénès	2014-04-30
*	Ltac repeat is in fact already doing progress	letouzey	2012-10-01
*	Updating headers.	herbelin	2012-08-08
*	Legacy Ring and Legacy Field migrated to contribs	letouzey	2012-07-05
*	Kills the useless tactic annotations "in \|- *"	letouzey	2012-07-05
*	Open Local Scope ---> Local Open Scope, same with Notation and alii	letouzey	2012-07-05
*	ZArith + other : favor the use of modern names instead of compat notations	letouzey	2012-07-05
*	theories/, plugins/ and test-suite/ ported to the Arguments vernacular	gareuselesinge	2011-11-21
*	Smaller proof terms for QcPower_{0,pos}	glondu	2011-08-17
*	Clean-up of Znumtheory, deletion of Zgcd_def	letouzey	2011-06-24
*	BinInt: Z.add become the alternative Z.add'	letouzey	2011-05-05
*	Modularization of BinPos + fixes in Stdlib	letouzey	2011-05-05
*	CompareSpec: a slight generalization/reformulation of CompSpec	letouzey	2011-03-17
*	First release of Vector library.	pboutill	2010-12-10
*	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