coq - The formal proof system

Age	Commit message (Collapse)	Author
2018-07-23	Make tokenize_string an optional parameter for diff methods in pp_diffs.	Jim Fehrle
	Remove forward reference to lexer.
2018-07-23	Displays the differences between successive proof steps in coqtop and CoqIDE.	Jim Fehrle
	Proof General requires minor changes to make the diffs visible, but this code shouldn't break the existing version of PG. Diffs are computed for the hypotheses and conclusion of the first goal between the old and new proofs. Strings are split into tokens using the Coq lexer, then the list of tokens are diffed using the Myers algorithm. A fixup routine (Pp_diff.shorten_diff_span) shortens the span of the diff result in some cases. Diffs can be enabled with the Coq commmand "Set Diffs on\|off\|removed." or "-diffs on\|off\|removed" on the OS command line. The "on" option shows only the new item with added text, while "removed" shows each modified item twice--once with the old value showing removed text and once with the new value showing added text. The highlights use 4 tags to specify the color and underline/strikeout. These are "diffs.added", "diffs.removed", "diffs.added.bg" and "diffs.removed.bg". The first two are for added or removed text; the last two are for unmodified parts of a modified item. Diffs that span multiple strings in the Pp are tagged with "start.diff." and "end.diff.", but only on the first and last strings of the span.
2018-07-23	Make the out_channel for the log file accessible so tests can write to it ↵	Jim Fehrle
	(e.g. for debugging)
2018-07-12	[dev] Autogenerate OCaml dev files.	Emilio Jesus Gallego Arias
	For now we only copy the templates, but we could do more fancy stuff. This helps to be compatible with build systems that take care of these files automatically, see: https://github.com/coq/coq/pull/6857#discussion_r202096579
2018-05-16	unit tests: add .merlin	Gaëtan Gilbert

2018-05-16	add unit tests to test suite	Paul Steckler