coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Emit a warning for void Arguments statement (Close 3713)	Enrico Tassi	2014-10-13
*	Parsing of "?[" as two tokens (makes ssr compile).	Enrico Tassi	2014-10-13
*	Fixing #3687 (inconsistent lexer state after a bullet).	Hugo Herbelin	2014-10-07
*	Seeing IntroWildcard as an action intro pattern rather than as a naming pattern	Hugo Herbelin	2014-09-30
*	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
*	Using an or_var rather than the hack with loc for coding a pure ident	Hugo Herbelin	2014-09-24
*	Add a "Hint Mode ref (+ \| -)*" hint for setting a global mode	Matthieu Sozeau	2014-09-15
*	Checking typability of evar instances. Using ";" to separate bindings	Hugo Herbelin	2014-09-13
*	Add syntax [id]: to apply tactic to goal named id.	Hugo Herbelin	2014-09-12
*	Parsing evar instances.	Hugo Herbelin	2014-09-12
*	Referring to evars by names. Added a parser for evars (but parsing of	Hugo Herbelin	2014-09-12