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
* \|	Merge branch 'v8.5' into trunk	Pierre Letouzey	2015-04-09
\|\\|
\| *	Declarative mode: plug the specialised printers back.	Arnaud Spiwack	2015-03-31
\| *	Better formatting of messages in proofs.	Arnaud Spiwack	2015-03-31
\| *	Generalisation of the "end command" argument of the goal printer.	Arnaud Spiwack	2015-03-31
* \|	Merge branch 'v8.5' into trunk	Enrico Tassi	2015-03-30
\|\\|
\| *	Putting the From parameter of the Require command into the AST.	Pierre-Marie Pédrot	2015-03-27
\| *	rewiring Czar printers that were disabled	Pierre Corbineau	2015-03-13
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-03-11
\|\\|
\| *	Do not display the status of monomorphic constants unless in universe-polymor...	Guillaume Melquiond	2015-03-09
* \|	rewiring Czar printers that were disabled	Pierre Corbineau	2015-03-02
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-02-23
\|\\|
\| *	Better English for #4070 implicit arguments message (thanks to Jason for his ...	Hugo Herbelin	2015-02-21
\| *	An answer to #4070 (message for implicit arguments of inl not clear).	Hugo Herbelin	2015-02-20
* \|	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-10
\|\\|
\| *	More efficient Richpp.	Pierre-Marie Pédrot	2015-02-06
\| *	Removing dead code.	Pierre-Marie Pédrot	2015-02-02
* \|	Merge branch 'v8.5' into trunk.	Pierre-Marie Pédrot	2015-01-25
\|\\|
\| *	Isolate a function for printing evar sets.	Hugo Herbelin	2015-01-24
* \|	Splitting ML tactics in one function per grammar entry.	Pierre-Marie Pédrot	2015-01-23
* \|	Embedding the index of the ML tactic entry in the Tacexpr AST.	Pierre-Marie Pédrot	2015-01-21
* \|	Univs: proper printing of global and local universe names (only	Matthieu Sozeau	2015-01-18
\| *	Univs: proper printing of global and local universe names (only	Matthieu Sozeau	2015-01-17
\|/
*	Fix issue in printing due to de Bruijn bug when constructing compatibility	Matthieu Sozeau	2015-01-13
*	Update headers.	Maxime Dénès	2015-01-12
*	Declarations.mli refactoring: module_type_body = module_body	Pierre Letouzey	2015-01-11
*	Continuing 785f82ee1 on reverting not only f5d7b2b1e but also	Hugo Herbelin	2015-01-08
*	Fixed and extend bullet related info/error messages. + doc.	Pierre Courtieu	2015-01-08
*	Revert "Term: include a function to print terms"	Enrico Tassi	2014-12-27
*	Term: include a function to print terms	Enrico Tassi	2014-12-26
*	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
*	Proof using: New vernacular to name sets of section variables	Enrico Tassi	2014-12-18
*	Fixed bad newlines in output for std output and emacs.	Pierre Courtieu	2014-12-18
*	msg_info now puts infomsg tag in emacs mode.	Pierre Courtieu	2014-12-16
*	Changed bullet informations to warning for better display in PG.	Pierre Courtieu	2014-12-15
*	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
*	Improving error message when one instance-hole is not found.	Hugo Herbelin	2014-12-04
*	Fixing printing of dirpathes in Ppconstr. It was reversed.	Pierre-Marie Pédrot	2014-11-30
*	Adding tag output to references in Ppconstr.	Pierre-Marie Pédrot	2014-11-25
*	Plugging console highlighting in for toplevel and compilation error messages.	Pierre-Marie Pédrot	2014-11-24
*	Removing useless flag of the historical move tactic.	Pierre-Marie Pédrot	2014-11-22