coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-05-09
\|\
\| *	Rename Lexer -> CLexer.	Pierre-Marie Pédrot	2016-05-09
* \|	Removing dead code and unused opens.	Pierre-Marie Pédrot	2016-05-08
* \|	Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...	Matthieu Sozeau	2016-04-04
\|\ \
* \| \|	Moving the Ltac definition command to an EXTEND based command.	Pierre-Marie Pédrot	2016-03-20
* \| \|	Moving Print Ltac to an EXTEND based command.	Pierre-Marie Pédrot	2016-03-20
* \| \|	Moving Tactic Notation to an EXTEND based command.	Pierre-Marie Pédrot	2016-03-20
* \| \|	Moving the parsing of the Ltac proof mode to G_ltac.	Pierre-Marie Pédrot	2016-03-19
* \| \|	Moving the proof mode parsing management to Pcoq.	Pierre-Marie Pédrot	2016-03-19
* \| \|	Moving Autorewrite to Hightatctic.	Pierre-Marie Pédrot	2016-03-06
* \| \|	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
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\\| \|
\| * \|	Update copyright headers.	Maxime Dénès	2016-01-20
* \| \|	Simplification of grammar_prod_item type.	Pierre-Marie Pédrot	2016-01-02
* \| \|	ALPHA-CONVERSION: in "parsing/g_vernac.ml4" file	Matej Kosik	2015-12-18
* \| \|	CLEANUP: Vernacexpr.vernac_expr	Matej Kosik	2015-12-18
\|/ /
* \|	Allowing empty bound universe variables.	Pierre-Marie Pédrot	2015-10-08
* \|	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
* \|	Record fields accept an optional final semicolon separator.	Pierre-Marie Pédrot	2015-10-07
* \|	Univs: Add universe binding lists to definitions	Matthieu Sozeau	2015-09-14
* \|	Hacking parser so as to support both [> ... ] and [id].	Hugo Herbelin	2015-09-08
\| *	Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080	Jason Gross	2015-08-14
\|/
*	Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"	Lionel Rieg	2015-06-26
*	Granting, undocumentedly, parsing of "Conjectures" as a synonym of	Hugo Herbelin	2015-06-16
*	Add a [Redirect] vernacular command	Clément Pit--Claudel	2015-05-04
*	Putting the From parameter of the Require command into the AST.	Pierre-Marie Pédrot	2015-03-27
*	Update headers.	Maxime Dénès	2015-01-12
*	Better doc and a few fixes for Proof using.	Enrico Tassi	2014-12-19
*	Proof using: New vernacular to name sets of section variables	Enrico Tassi	2014-12-18
*	About now accepts hypothesis names and goal selector.	Pierre Courtieu	2014-12-15
*	Searchxxx now search also the hypothesis and support goal selector.	Pierre Courtieu	2014-12-12
*	Switch the few remaining iso-latin-1 files to utf8	Pierre Letouzey	2014-12-09
*	Add [Info] command.	Arnaud Spiwack	2014-11-01
*	Emit a warning for void Arguments statement (Close 3713)	Enrico Tassi	2014-10-13
*	Add syntax for naming new goals in refine: writing ?[id] instead of _	Hugo Herbelin	2014-09-30
*	Notation: option to attach extra pretty printing rules to notations	Enrico Tassi	2014-09-29
*	Add syntax [id]: to apply tactic to goal named id.	Hugo Herbelin	2014-09-12
*	Factorize the parsing rules of [Record] and the other kind of type definitions.	Arnaud Spiwack	2014-09-04
*	Remove [Infer] option of records.	Arnaud Spiwack	2014-09-04
*	Add a [Variant] declaration which allows to write non-recursive variant types.	Arnaud Spiwack	2014-09-04
*	Fixing bug #3493.	Pierre-Marie Pédrot	2014-08-27
*	Uncountably many bullets (+,-,,++,--,*,+++,...).	Hugo Herbelin	2014-08-05
*	STM: new "par:" goal selector, like "all:" but in parallel	Enrico Tassi	2014-08-05
*	Adding a new "Locate Term" command, distinct from the raw "Locate" command.	Pierre-Marie Pédrot	2014-07-21
*	Add toplevel commands to declare global universes and constraints.	Matthieu Sozeau	2014-07-01
*	Fix bug #3289	Matthieu Sozeau	2014-06-11
*	Remove the syntax [Vernac1. Vernac2. … Vernacn. ].	Arnaud Spiwack	2014-06-06
*	Adapt Y. Bertot's path on private inductives (now the keyword is "Private").	Yves Bertot	2014-05-06