coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	- Fix printing and parsing of primitive projections, including the Set	Matthieu Sozeau	2014-09-09
*	Removing the XML plugin.	Pierre-Marie Pédrot	2014-09-08
*	"allows to", like "allowing to", is improper	Jason Gross	2014-08-25
*	Instead of relying on a trick to make the constructor tactic parse, put	Pierre-Marie Pédrot	2014-08-07
*	Removing the "constructor" tactic from the AST.	Pierre-Marie Pédrot	2014-08-07
*	Experimentally adding an option for automatically erasing an	Hugo Herbelin	2014-08-05
*	Arith: full integration of the "Numbers" modular framework	Pierre Letouzey	2014-07-09
*	Basic lemmas about the algebraic structure of equality.	Hugo Herbelin	2014-05-31
*	Moving argument-free tactics out of the AST into a dedicated	Pierre-Marie Pédrot	2014-05-16
*	Now parsing rules of ML-declared tactics are only made available after the	Pierre-Marie Pédrot	2014-05-12
*	Removing comment outdated since eta holds in conversion rule (this	Hugo Herbelin	2014-05-07
*	Try a new way of handling template universe levels	Matthieu Sozeau	2014-05-06
*	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	No more Coersion in Init.	Pierre Boutillier	2014-04-10
*	Define [projT3] and [proj3_sig]	Jason Gross	2014-04-10
*	[Coercion]s use [Sortclass], not [Prop] (in docs)	Jason Gross	2014-01-24
*	Better unification for [projT1] and [proj1_sig].	Jason Gross	2013-12-12
*	Adding Acc_intro_generator in order to help computations of Function in parti...	forest	2013-11-20
*	Side effect free implementation of admit (Isabelle's oracle)	gareuselesinge	2013-08-08
*	Improving printing of 'rew' notation	herbelin	2013-05-05
*	Relaxing the constraint on eta-expanding on the fly while looking for	herbelin	2013-05-05
*	Added group properties of eq_refl, eq_sym, eq_trans	herbelin	2013-04-17
*	Unset Asymmetric Patterns	pboutill	2013-01-18
*	nat_iter n f x -> nat_rect _ x (fun _ => f) n	pboutill	2012-12-21
*	Some lemmas on property of rewriting. It will probably be worth at	herbelin	2012-11-15
*	Change Hint Resolve, Immediate to take a global reference as argument	msozeau	2012-10-26
*	Removed a few calls to "Opaque" in Logic.v ineffective since at least	herbelin	2012-10-24
*	No more states/initial.coq, instead coqtop now requires Prelude.vo	letouzey	2012-08-23
*	Updating headers.	herbelin	2012-08-08
*	induction/destruct : nicer syntax for generating equations (solves #2741)	letouzey	2012-07-09
*	Kills the useless tactic annotations "in \|- *"	letouzey	2012-07-05
*	ZArith + other : favor the use of modern names instead of compat notations	letouzey	2012-07-05
*	Notation: a new annotation "compat 8.x" extending "only parsing"	letouzey	2012-07-05
*	Bug 2767	pboutill	2012-05-09
*	Remove the Dp plugin.	gmelquio	2012-04-17
*	"A -> B" is a notation for "forall _ : A, B".	pboutill	2012-04-12
*	Fixing a few bugs (see #2571) related to interpretation of multiple binders	herbelin	2012-04-06
*	Final part of moving Program code inside the main code. Adapted add_definitio...	msozeau	2012-03-14
*	No more use of tauto in Init/	pboutill	2012-01-19
*	theories/, plugins/ and test-suite/ ported to the Arguments vernacular	gareuselesinge	2011-11-21
*	SearchAbout and similar: add a customizable blacklist	letouzey	2011-08-11
*	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-10
*	Moved the declaration of "Classic" being the default proof mode to coqtop.ml ...	aspiwack	2011-08-09
*	New proposition "rewrite Heq in H" for eq_rect (assuming that there is	herbelin	2011-08-08
*	All the parameters of or can be implicits.	pboutill	2011-07-26
*	Same Implicit Arguments rule for sumbool and sumor.	pboutill	2011-07-26
*	Tentative abbreviation "rew Heq in H" for eq_rect. (feedback welcome)	herbelin	2011-07-16
*	Added a characterization of unique existence.	herbelin	2011-07-16