coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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 remote-tracking branch 'origin/v8.5' into trunk	Hugo Herbelin	2015-09-09
\|\\|
\| *	Hacking parser so as to support both [> ... ] and [id].	Hugo Herbelin	2015-09-08
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-07-27
\|\\|
\| *	Removing the G_xml module again.	Pierre-Marie Pédrot	2015-07-22
* \|	Merge branch 'v8.5' into trunk	Maxime Dénès	2015-07-02
\|\\|
\| *	Notation: use same level for "@" in constr: and pattern: (Close: #4272)	Enrico Tassi	2015-07-01
* \|	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
* \|	Merge remote-tracking branch 'forge/v8.5'	Pierre Boutillier	2015-06-22
\|\\|
\| *	Granting, undocumentedly, parsing of "Conjectures" as a synonym of	Hugo Herbelin	2015-06-16
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-05-05
\|\\|
\| *	Add a [Redirect] vernacular command	Clément Pit--Claudel	2015-05-04
\| *	Remove almost all the uses of string concatenation when building error messages.	Guillaume Melquiond	2015-04-23
\| *	Inlining "fun" and "forall" tokens in parser, so that alternative notations for	Hugo Herbelin	2015-04-20
* \|	Merge branch 'v8.5' into trunk	Enrico Tassi	2015-03-30
\|\\|
\| *	grammar: export constr_eval	Enrico Tassi	2015-03-30
\| *	grammar: export hypident	Enrico Tassi	2015-03-30
\| *	Putting the From parameter of the Require command into the AST.	Pierre-Marie Pédrot	2015-03-27
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-03-23
\|\\|
\| *	Qed export -> Qed exporting	Enrico Tassi	2015-03-22
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-02-26
\|\\|
\| *	Fixed 3233 (fresh does not work with a qualid).	Pierre Courtieu	2015-02-23
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-02-15
\|\\|
\| *	Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior	Enrico Tassi	2015-02-14
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-02-13
\|\\|
\| *	Fixing #3982 (conflict with max notation for universes).	Hugo Herbelin	2015-02-12
* \|	Embedding the index of the ML tactic entry in the Tacexpr AST.	Pierre-Marie Pédrot	2015-01-21
\|/
*	Update headers.	Maxime Dénès	2015-01-12
*	A global [gfail] tactic which works like [fail] except that it fails even if ...	Arnaud Spiwack	2014-12-23
*	Fix compilation error in some configurations.	Arnaud Spiwack	2014-12-23
*	Add a backtracking version of Ltac's [match].	Arnaud Spiwack	2014-12-19
*	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
*	Fixing CAMLP4 compilation.	Pierre-Marie Pédrot	2014-12-16
*	Getting rid of Exninfo hacks.	Pierre-Marie Pédrot	2014-12-16
*	About now accepts hypothesis names and goal selector.	Pierre Courtieu	2014-12-15
*	Add Ltac syntax for the [tclIFCATCH] primitive.	Arnaud Spiwack	2014-12-12
*	Extend the syntax of simpl with a delta flag.	Arnaud Spiwack	2014-12-12
*	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
*	Enforcing a stronger difference between the two syntaxes "simpl	Hugo Herbelin	2014-11-16
*	Removing a unused boolean in the TacMove node of tacexpr AST.	Pierre-Marie Pédrot	2014-11-09
*	Fixing bugs #3723 and #3787 (reinitialization of camlp5 empty levels)	Hugo Herbelin	2014-11-06
*	Supporting "at occs" as a short-hand for "in \|- * at occs" in "destruct".	Hugo Herbelin	2014-11-02
*	Add [Info] command.	Arnaud Spiwack	2014-11-01
*	Reorganization of the test for generic selection of occurrences in	Hugo Herbelin	2014-10-31
*	Dead code	Hugo Herbelin	2014-10-27
*	This commit introduces changes in induction and destruct.	Hugo Herbelin	2014-10-25