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
\| * \| \|	Revert the four previous commits and update the description of Richpp.	Pierre-Marie Pédrot	2015-08-15
\| * \| \|	More invariants in Richpp.	Pierre-Marie Pédrot	2015-08-15
\| * \| \|	More parametric type for generalized XML.	Pierre-Marie Pédrot	2015-08-15
\| \| * \|	Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080	Jason Gross	2015-08-14
\| \|/ / \|/\| \|
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-07-27
\|\\| \|
\| * \|	Fixing bug #2169:	Pierre-Marie Pédrot	2015-07-27
* \| \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-07-18
\|\\| \|
\| * \|	Fixing printing of primitive coinductive record status.	Pierre-Marie Pédrot	2015-07-09
* \| \|	Merge branch 'v8.5' into trunk	Maxime Dénès	2015-07-02
\|\\| \|
\| * \|	Assumptions: more informative print for False axiom (Close: #4054)	Enrico Tassi	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
\| * \|	Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.	Thomas Sibut-Pinote	2015-06-25
\| \| *	Make inductives that were assumed positive appear in `Print Assumptions`.	Arnaud Spiwack	2015-06-24
\| \| *	Add corresponding field in `VernacInductive`.	Arnaud Spiwack	2015-06-24
\| \|/ \|/\|
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-06-24
\|\\|
\| *	Add a space in cast since cast binds loosely.	Gregory Malecha	2015-06-24
* \|	Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.	Thomas Sibut-Pinote	2015-06-23
* \|	Merge remote-tracking branch 'forge/v8.5'	Pierre Boutillier	2015-06-22
\|\\|
\| *	Make end-of-proof output consistent across toplevels.	Guillaume Melquiond	2015-06-19
* \|	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