coq - The formal proof system

Age	Commit message (Collapse)	Author
2018-10-04	Test-suite: avoid explicit references to “Top”	Vincent Laporte

2017-04-05	[toplevel] Remove exception error printer in favor of feedback printer.	Emilio Jesus Gallego Arias
	We solve https://coq.inria.fr/bugs/show_bug.cgi?id=4789 by printing all the errors from the feedback handler, even in the case of coqtop. All error display is handled by a single, uniform path. There may be some minor discrepancies with 8.6 as we are uniform now whereas 8.6 tended to print errors in several ways, but our behavior is a subset of the 8.6 behavior. We had to make a choice for `-emacs` error output, which used to vary too. We have chosen to display error messages as: ``` (location info) option \n (program caret) option \n MARKER[254]Error: msgMARKER[255] ``` This commit also fixes: - https://coq.inria.fr/bugs/show_bug.cgi?id=5418 - https://coq.inria.fr/bugs/show_bug.cgi?id=5429
2016-10-17	Fix output test for module qualification.	Pierre-Marie Pédrot
	The output was embedding local paths from my machine.
2016-10-17	Test for bug #4874.	Pierre-Marie Pédrot