coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
\|\ \ \
\| \| \| *	[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
\| \|_\|/ \|/\| \|
* \| \|	Merge PR#134: Enable `-safe-string`	Maxime Dénès	2017-03-21
\|\ \ \
* \| \| \|	trivial: fix comment	Matej Kosik	2017-03-21
\| * \| \|	[misc] Remove warnings about String.set	Emilio Jesus Gallego Arias	2017-03-20
* \| \| \|	Merge PR#479: [future] Remove unused parameter greedy.	Maxime Dénès	2017-03-20
\|\ \ \ \
* \ \ \ \	Merge PR#487: Add a forgotten (?) line to "theories/Logic/vo.itarget".	Maxime Dénès	2017-03-19
\|\ \ \ \ \
\| * \| \| \| \|	Add a forgotten (?) line to "theories/Logic/vo.itarget".	Matej Kosik	2017-03-19
\|/ / / / /
* \| \| \| \|	Merge PR#428: Report missing tactic arguments in error message	Maxime Dénès	2017-03-17
\|\ \ \ \ \
* \ \ \ \ \	Merge PR#437: Improve unification debug trace.	Maxime Dénès	2017-03-17
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR#445: TACTIC EXTEND now takes an optional level as argument.	Maxime Dénès	2017-03-17
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR#442: Allow interactive editing of Coq.Init.Logic	Maxime Dénès	2017-03-17
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR#451: Add η principles for sigma types	Maxime Dénès	2017-03-17
\|\ \ \ \ \ \ \ \ \
* \| \| \| \| \| \| \| \| \|	Attempt to improve error message when "apply in" fail.	Hugo Herbelin	2017-03-15
* \| \| \| \| \| \| \| \| \|	Merge PR#267: Proposal for an update of the recommended style in programming ...	Maxime Dénès	2017-03-15
\|\ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| * \| \|	[safe-string] Enable -safe-string !	Emilio Jesus Gallego Arias	2017-03-14
\| \| \| \| \| \| \| \| * \| \|	[safe-string] tools	Emilio Jesus Gallego Arias	2017-03-14
\| \| \| \| \| \| \| \| * \| \|	[safe-string] ide	Emilio Jesus Gallego Arias	2017-03-14
\| \| \| \| \| \| \| \| * \| \|	[safe-string] plugins/extraction	Emilio Jesus Gallego Arias	2017-03-14
\| \| \| \| \| \| \| \| * \| \|	[safe-string] ltac/profile_ltac	Emilio Jesus Gallego Arias	2017-03-14
\| \| \| \| \| \| \| \| * \| \|	[safe_string] toplevel/vernac	Emilio Jesus Gallego Arias	2017-03-14