coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Revert "Adding option "Set Reversible Pattern Implicit" to Specif.v so that an"	Hugo Herbelin	2016-04-27
*	Adding option "Set Reversible Pattern Implicit" to Specif.v so that an	Hugo Herbelin	2016-04-27
*	Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...	Matthieu Sozeau	2016-04-04
\|\
* \|	Moving Eauto to a simple ML file.	Pierre-Marie Pédrot	2016-03-06
* \|	Moving tauto.ml4 to a proper ML file.	Pierre-Marie Pédrot	2016-02-23
* \|	Moving the Tauto tactic to proper Ltac.	Pierre-Marie Pédrot	2016-02-22
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\ \
\| * \|	Update copyright headers.	Maxime Dénès	2016-01-20
* \| \|	Removing auto from the tactic AST.	Pierre-Marie Pédrot	2015-12-24
\| * \|	Remove Print Universe directive.	Matthieu Sozeau	2015-10-02
\| * \|	Universes: enforce Set <= i for all Type occurrences.	Matthieu Sozeau	2015-10-02
\| \| *	Move type_scope into user space, fix some output logs	Jason Gross	2015-08-14
\| \| *	Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080	Jason Gross	2015-08-14
\| \|/ \|/\|
\| *	Reverting 16 last commits, committed mistakenly using the wrong push command.	Hugo Herbelin	2015-08-02
\| *	Adding a notation { x & P } for { x : _ & P }.	Hugo Herbelin	2015-08-02
* \|	Tentatively setting cons and Some with 1st implicit argument maximal	Hugo Herbelin	2015-05-09
\|/
*	Fix various typos in documentation	Matěj Grabovský	2015-03-31
*	admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)	Enrico Tassi	2015-03-11
*	Reorder the steps of the easy tactic. (Fix for bug #2630)	Guillaume Melquiond	2015-02-25
*	Correct restriction of vm_compute when handling universe polymorphic	Matthieu Sozeau	2015-01-15
*	Update headers.	Maxime Dénès	2015-01-12
*	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-11-02
*	eta contractions	Pierre Boutillier	2014-10-01
*	- 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