coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| \| \| \| \| \| \| \| \| \| * \| \| \| \|	make check not CoqIDE-specific	Paul Steckler	2017-03-22
\| \| \| \| \| \| \| \| \| \| \|/ / / /
* \| \| \| \| \| \| \| \| \| / / / /	Better compatibility of TACTIC EXTEND AT LEVEL with versions of camlp5.	Hugo Herbelin	2017-03-22
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / \|/\| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| * \| \| \| \|	[travis] Fix iris-coq build.	Emilio Jesus Gallego Arias	2017-03-22
\| \|_\|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \|	Document the changes to IZR.	Guillaume Melquiond	2017-03-22
\| * \| \| \| \| \| \| \| \| \| \|	Make IZR a morphism for field.	Guillaume Melquiond	2017-03-22
\| * \| \| \| \| \| \| \| \| \| \|	Mark ring morphisms as opaque.	Guillaume Melquiond	2017-03-22
\| * \| \| \| \| \| \| \| \| \| \|	Change the parser and printer so that they use IZR for real constants.	Guillaume Melquiond	2017-03-22
\| \| \| \| \| \| \| * \| \| \| \|	[travis] [8.6.only] Backport latest changes from trunk.	Emilio Jesus Gallego Arias	2017-03-22
\| \| \| \| \|_\|_\|/ / / / / \| \| \| \|/\| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \|	Make IZR use a compact representation of integers.	Guillaume Melquiond	2017-03-22
\| * \| \| \| \| \| \| \| \| \|	Fix broken evaluation strategies for ring and field.	Guillaume Melquiond	2017-03-22
\| * \| \| \| \| \| \| \| \| \|	Fix some typos.	Guillaume Melquiond	2017-03-22
\| * \| \| \| \| \| \| \| \| \|	Simplify some proofs using ring and field.	Guillaume Melquiond	2017-03-22
\| * \| \| \| \| \| \| \| \| \|	Remove duplicate lemmas.	Guillaume Melquiond	2017-03-22
\|/ / / / / / / / / /
\| \| \| \| \| * / / / /	funind: Ignore missing info for current function	Tej Chajed	2017-03-22
\| \| \| \|_\|/ / / / / \| \| \|/\| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-03-22
\|\ \ \ \ \ \ \ \ \ \| \| \|/ / / / / / / \| \|/\| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Merge PR#390: Updates to the Pretty Printing Infrastructure	Maxime Dénès	2017-03-22
\|\ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \	Merge PR#478: Small optimization on handling of library state.	Maxime Dénès	2017-03-22
\|\ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \	Merge PR#482: [toplevel] Remove unusable option -notop	Maxime Dénès	2017-03-22
\|\ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| * \| \| \| \|	Add a few comments in term_typing.ml.	Maxime Dénès	2017-03-21
\| \| \| \| \| \| \| * \| \| \| \|	Do not typecheck twice the type of opaque constants.	Maxime Dénès	2017-03-21
\| \| \| \| \| \|_\|/ / / / / \| \| \| \| \|/\| \| \| \| \| \|
\| \| \| * \| \| \| \| \| \| \|	[ide protocol] Add comment about leftover parameter.	Emilio Jesus Gallego Arias	2017-03-21
\| \| \| * \| \| \| \| \| \| \|	[pp] Hide the internal representation of `std_ppcmds`.	Emilio Jesus Gallego Arias	2017-03-21
\| \| \| * \| \| \| \| \| \| \|	[pp] Fix bug in richpp Format use.	Emilio Jesus Gallego Arias	2017-03-21
\| \| \| * \| \| \| \| \| \| \|	[extraction] Flush formatters at end of output.	Emilio Jesus Gallego Arias	2017-03-21
\| \| \| * \| \| \| \| \| \| \|	[xml] Restore protocol compatibility with 8.6.	Emilio Jesus Gallego Arias	2017-03-21
\| \| \| * \| \| \| \| \| \| \|	[stm] Add common toploop for workers.	Emilio Jesus Gallego Arias	2017-03-21
\| \| \| * \| \| \| \| \| \| \|	[pp] Remove uses of expensive string_of_ppcmds.	Emilio Jesus Gallego Arias	2017-03-21
\| \| \| * \| \| \| \| \| \| \|	[pp] [ide] Minor cleanups in pp code.	Emilio Jesus Gallego Arias	2017-03-21
\| \| \| * \| \| \| \| \| \| \|	[pp] Move terminal-specific tagging to the toplevel.	Emilio Jesus Gallego Arias	2017-03-21
\| \| \| * \| \| \| \| \| \| \|	[pp] Remove special tag type and handler from Pp.	Emilio Jesus Gallego Arias	2017-03-21
\| \| \| * \| \| \| \| \| \| \|	[ide] Dynamic printing width.	Emilio Jesus Gallego Arias	2017-03-21
\| \| \| * \| \| \| \| \| \| \|	[ide] richpp clenaup	Emilio Jesus Gallego Arias	2017-03-21
\| \| \| * \| \| \| \| \| \| \|	[pp] Debug feeder is not needed anymore.	Emilio Jesus Gallego Arias	2017-03-21
\| \| \| * \| \| \| \| \| \| \|	[pp] Remove richpp from fake_ide.	Emilio Jesus Gallego Arias	2017-03-21
\| \| \| * \| \| \| \| \| \| \|	[pp] Make feedback the only logging mechanism.	Emilio Jesus Gallego Arias	2017-03-21
\| \| \| * \| \| \| \| \| \| \|	[error] Move back fatal_error to toplevel	Emilio Jesus Gallego Arias	2017-03-21
\| \| \| * \| \| \| \| \| \| \|	[feedback] Allow to remove feedback listeners.	Emilio Jesus Gallego Arias	2017-03-21
\| \| \| * \| \| \| \| \| \| \|	[pp] Remove redundant white spacing pp construct.	Emilio Jesus Gallego Arias	2017-03-21
\| \| \| * \| \| \| \| \| \| \|	[pp] Force well-formed boxes by construction.	Emilio Jesus Gallego Arias	2017-03-21
\| \| \| * \| \| \| \| \| \| \|	[pp] Force well-tagged docs by construction.	Emilio Jesus Gallego Arias	2017-03-21
\| \| \| * \| \| \| \| \| \| \|	[pp] Implement n-ary glue.	Emilio Jesus Gallego Arias	2017-03-21
\| \| \| * \| \| \| \| \| \| \|	[pp] Make pp public to allow serialization.	Emilio Jesus Gallego Arias	2017-03-21
\| \| \| * \| \| \| \| \| \| \|	[pp] Prepare for serialization, remove opaque glue.	Emilio Jesus Gallego Arias	2017-03-21
\| \| \| * \| \| \| \| \| \| \|	[pp] Remove `Pp.stras`.	Emilio Jesus Gallego Arias	2017-03-21
\| \| \| * \| \| \| \| \| \| \|	[pp] Replace `Pp.Tag` by `Ppstyle.tag` = `string list`	Emilio Jesus Gallego Arias	2017-03-21
\| \| \| * \| \| \| \| \| \| \|	[pp] Remove unused printing tagging infrastructure.	Emilio Jesus Gallego Arias	2017-03-21
\| \| \| * \| \| \| \| \| \| \|	[ide] ide_slave doesnt't need to capture stdout	Emilio Jesus Gallego Arias	2017-03-21
\| \| \| * \| \| \| \| \| \| \|	[ide] Use "log via feedback".	Emilio Jesus Gallego Arias	2017-03-21
\| \|_\|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \|	[safe-string] update dev/doc/changes	Emilio Jesus Gallego Arias	2017-03-21
\| \|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Merge PR#134: Enable `-safe-string`	Maxime Dénès	2017-03-21
\|\ \ \ \ \ \ \ \ \