coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-29
\|\
\| *	Implement support for universe binder lists in Instance and Program Fixpoint/...	Matthieu Sozeau	2016-01-23
* \|	New step on recent 9c2662eecc398f3 (strong invariants on tuple pattern).	Hugo Herbelin	2016-01-21
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\|
* \|	Stronger invariants on the use of the introduction pattern (pat1,...,patn).	Hugo Herbelin	2016-01-21
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	Separating the parsing of user-defined entries from their intepretation.	Pierre-Marie Pédrot	2016-01-16
* \|	CLEANUP: removing unnecessary wrapper	Matej Kosik	2016-01-11
* \|	COMMENTS: added to the "Constrexpr.CCases" variant.	Matej Kosik	2016-01-11
* \|	CLEANUP: removing unused field	Matej Kosik	2016-01-11
* \|	Simplification of grammar_prod_item type.	Pierre-Marie Pédrot	2016-01-02
* \|	Separation of concern in TacAlias API.	Pierre-Marie Pédrot	2016-01-02
* \|	External tactics and notations now accept any tactic argument.	Pierre-Marie Pédrot	2015-12-30
* \|	Removing auto from the tactic AST.	Pierre-Marie Pédrot	2015-12-24
* \|	CLEANUP: the definition of the "Constrexpr.case_expr" type was simplified	Matej Kosik	2015-12-18
* \|	CLEANUP: removing unnecessary alias	Matej Kosik	2015-12-18
* \|	CLEANUP: Vernacexpr.VernacDeclareTacticDefinition	Matej Kosik	2015-12-18
* \|	CLEANUP: Removing "Vernacexpr.VernacNop" variant to which no Vernacular comma...	Matej Kosik	2015-12-18
* \|	COMMENTS: added to some variants of "Misctypes.glob_sort_gen" type.	Matej Kosik	2015-12-18
* \|	COMMENTS: added to some variants of "Glob_term.glob_constr" type.	Matej Kosik	2015-12-18
* \|	COMMENTS: added to some variants of the "Constrexpr.prim_token" type.	Matej Kosik	2015-12-18
* \|	CLEANUP: Vernacexpr.vernac_expr	Matej Kosik	2015-12-18
* \|	Getting rid of the dynamic node of the tactic AST.	Pierre-Marie Pédrot	2015-12-04
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-12-03
\|\\|
\| *	Dead code from August 2014 in apply in.	Hugo Herbelin	2015-12-02
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-11-05
\|\\|
\| *	Adding syntax "Show id" to show goal named id (shelved or not).	Hugo Herbelin	2015-11-02
* \|	Fixing the return type of the Atoken symbol.	Pierre-Marie Pédrot	2015-10-28
* \|	Type-safe grammar extensions.	Pierre-Marie Pédrot	2015-10-27
* \|	Type delayed_open_constr is now monotonic.	Pierre-Marie Pédrot	2015-10-19
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-12
\|\\|
\| *	Fixing untimely unexpected warning "Collision between bound variables" (#4317).	Hugo Herbelin	2015-10-11
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-09
\|\\|
\| *	Axioms now support the universe binding syntax.	Pierre-Marie Pédrot	2015-10-08
\| *	Proof using: let-in policy, optional auto-clear, forward closure*	Enrico Tassi	2015-10-08
\| *	Goptions: new value type: optional string	Enrico Tassi	2015-10-08
\| *	Univs: add Strict Universe Declaration option (on by default)	Matthieu Sozeau	2015-10-07
* \|	Merge branch 'v8.5' into trunk	Maxime Dénès	2015-09-17
\|\\|
\| *	Univs: Add universe binding lists to definitions	Matthieu Sozeau	2015-09-14
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-08-22
\|\\|
\| *	Documentation by giving a name to a large type.	Pierre-Marie Pédrot	2015-08-19
* \|	Merge branch 'v8.5' into trunk	Maxime Dénès	2015-07-02
\|\\|
\| *	Code documentation of the TACTIC/VERNAC EXTEND macros.	Pierre-Marie Pédrot	2015-06-29
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-06-28
\|\\|
\| *	Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"	Lionel Rieg	2015-06-26
* \|	Remove other types not carried by interpretations in `Tacexpr`.	Arnaud Spiwack	2015-06-25
* \|	Remove useless `and_short_name` in interpreted level in `Tacexpr`.	Arnaud Spiwack	2015-06-25
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-05-05
\|\\|
\| *	Add a [Redirect] vernacular command	Clément Pit--Claudel	2015-05-04
* \|	Merge branch 'v8.5' into trunk	Enrico Tassi	2015-03-30
\|\\|