coq - The formal proof system

Age	Commit message (Expand)	Author
2016-01-20	Update copyright headers.	Maxime Dénès
2015-10-02	Remove Print Universe directive.	Matthieu Sozeau
2015-10-02	Universes: enforce Set <= i for all Type occurrences.	Matthieu Sozeau
2015-03-11	admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)	Enrico Tassi
2015-01-12	Update headers.	Maxime Dénès
2014-11-02	Improving elimination with indices, getting rid of intrusive residual	Hugo Herbelin
2014-11-02	Supporting "at occs" as a short-hand for "in \|- * at occs" in "destruct".	Hugo Herbelin
2014-05-31	Basic lemmas about the algebraic structure of equality.	Hugo Herbelin
2014-05-07	Removing comment outdated since eta holds in conversion rule (this	Hugo Herbelin
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2013-08-08	Side effect free implementation of admit (Isabelle's oracle)	gareuselesinge
2013-05-05	Improving printing of 'rew' notation	herbelin
2013-04-17	Added group properties of eq_refl, eq_sym, eq_trans	herbelin
2012-11-15	Some lemmas on property of rewriting. It will probably be worth at	herbelin
2012-10-24	Removed a few calls to "Opaque" in Logic.v ineffective since at least	herbelin
2012-08-08	Updating headers.	herbelin
2012-07-05	Kills the useless tactic annotations "in \|- *"	letouzey
2012-07-05	Notation: a new annotation "compat 8.x" extending "only parsing"	letouzey
2012-04-12	"A -> B" is a notation for "forall _ : A, B".	pboutill
2012-04-06	Fixing a few bugs (see #2571) related to interpretation of multiple binders	herbelin
2012-01-19	No more use of tauto in Init/	pboutill
2011-11-21	theories/, plugins/ and test-suite/ ported to the Arguments vernacular	gareuselesinge
2011-08-10	Take benefit of bullets available by default in Prelude	herbelin
2011-08-10	Less ambitious application of a notation for eq_rect. We proposed	herbelin
2011-08-08	New proposition "rewrite Heq in H" for eq_rect (assuming that there is	herbelin
2011-07-26	All the parameters of or can be implicits.	pboutill
2011-07-16	Tentative abbreviation "rew Heq in H" for eq_rect. (feedback welcome)	herbelin
2011-07-16	Added a characterization of unique existence.	herbelin
2010-10-23	Used multiple lists of implicit arguments to transfer the choices of	herbelin
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-07-22	Made notations for exists, exists! and notations of Utf8.v recursive notations	herbelin
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2010-01-08	Init/Logic: commutativity and associativity of /\ and \/	letouzey
2009-10-08	Implicit argument of Logic.eq become maximally inserted	letouzey
2009-01-01	Switched to "standardized" names for the properties of eq and	herbelin
2008-12-28	- Another bug in get_sort_family_of (sort-polymorphism of constants and	herbelin
2008-12-26	- Optimized "auto decomp" which had a (presumably) exponential in	herbelin
2007-11-08	Moved several lemmas from theories/Numbers/NumPrelude to theories/Init/Logic.	emakarov
2007-10-03	Révision de theories/Logic concernant les axiomes de descriptions.	herbelin
2007-09-30	Ajout infos de débogage de "universe inconsistency" quand option Set	herbelin
2006-10-17	Mise en forme des theories	notin
2006-08-28	Passage à une définition de inhabited plus dans les 'standard mathématique...	herbelin
2006-06-09	Modification déf de exists! pour éviter une éta-expansion et pouvoir être...	herbelin
2006-06-04	Remplacement 'singleton' par 'unique' as a simple way to avoid a conflict wit...	herbelin
2006-06-04	Ajout exists! et restructuration/extension des fichiers sur la	herbelin
2006-03-17	Modification des propriétés (svn:executable)	notin
2006-03-04	Titres moins envahissants pour coqdoc	herbelin
2006-02-23	Ajout 'exists! x:A, P (suite)	herbelin
2006-02-23	Ajout 'exists! x:A, P	herbelin
2006-02-10	code mort	herbelin