coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\|
*	Update copyright headers.	Maxime Dénès	2016-01-20
\|
*	Fix width of underscore in coq_tex output.	Guillaume Melquiond	2015-07-30
\|
*	Fix broken regexp.	Guillaume Melquiond	2015-07-30
\| \| \| \| \|	Characters do not need to be escaped in character ranges. It just had the effect of matching backslashes four times.
*	Remove unused variables.	Guillaume Melquiond	2015-07-30
\|
*	Remove usage of Printexc.catch in the tools, as it is deprecated since 2001.	Guillaume Melquiond	2015-07-30
\| \| \| \| \| \| \| \|	"This function is deprecated: the runtime system is now able to print uncaught exceptions as precisely as Printexc.catch does. Moreover, calling Printexc.catch makes it harder to track the location of the exception using the debugger or the stack backtrace facility. So, do not use Printexc.catch in new code."
*	Make coq-tex more robust with respect to the (non-)command on the last line.	Guillaume Melquiond	2015-07-29
\|
*	Remove empty commands from the output of coq-tex.	Guillaume Melquiond	2015-07-29
\|
*	Rewrite the main loop of coq-tex.	Guillaume Melquiond	2015-07-29
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Before this commit, coq-tex was reading the .v file and was guessing how many lines from the coqtop output it should display. Now, it reads the coqtop output and it guesses how many lines from the .v file it should display. That way, coq-tex no longer needs to embed a parser; it relies on coqtop for parsing. This is much more robust and makes it possible to properly handle script such as the following one: Goal { True } + { False }. { left. exact I. } As before, if there is a way for a script to produce something that looks like a prompt (that is, a line that starts with "foo < "), coq-tex will be badly confused.
*	Make coq-tex aware of lines ending with "}", so as to fix the FAQ.	Guillaume Melquiond	2015-07-28
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This is only a heuristic and it might cause the tool to become awfully confused if a line ends with "}" yet this is not the end of a tactic block. Fixing it would require a full-blown Coq parser inside coq-tex. Example of crazy output: Coq < Goal { True } Coq < 1 subgoal ============================ {True} + {False} Coq < + { False }.
*	Fix command-line documentation of coq-tex.	Guillaume Melquiond	2015-07-08
\|
*	Prevent Latex from messing with backticks. (Fix for bug #3871)	Guillaume Melquiond	2015-02-10
\|
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	Reduce the amount of "Coq <" prompts generated by coq_tex. (Partial fix for ↵	Guillaume Melquiond	2014-04-28
\| \| \| \|	bug #2964)
*	Prevent coq_tex from generating curly quotes. (Partial fix for bug #2964)	Guillaume Melquiond	2014-04-28
\|
*	Getting rid of the use of deprecated elements (from the OCaml standard library).	xclerc	2013-10-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16882 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Restrict (try...with...) to avoid catching critical exn (part 13)	letouzey	2013-03-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16290 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Allow running coq-tex in win32 (fix #2921)	letouzey	2012-10-29
	Yes, it seems that < and > and even 2>&1 are legal under windows :-) Btw, the only function using streams has been rewritten, so coq_tex is now a standard .ml file, not a .ml4 anymore (beware during upgrade!) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15938 85f007b7-540e-0410-9357-904b9bb8a0f7