coq - The formal proof system

Age	Commit message (Collapse)	Author
2019-02-28	Show diffs in error messages if color is enabled	Jim Fehrle

2018-12-09	[doc] Enable Warning 50 [incorrect doc comment] and fix comments.	Emilio Jesus Gallego Arias
	This is a pre-requisite to use automated formatting tools such as `ocamlformat`, also, there were quite a few places where the comments had basically no effect, thus it was confusing for the developer. p.s: Reading some comments was a lot of fun :)
2018-11-21	[legacy proof engine] Remove some cruft.	Emilio Jesus Gallego Arias
	We remove the `Proof_types` file which was a trivial stub, we also cleanup a few layers of aliases. This is not a lot but every little step helps.
2018-09-20	Current diff code only compares the first current goal of the old and new	Jim Fehrle
	proof states. That's not always correct. This change will a) show diffs for all displayed goals and b) correctly match goals between the old and new proof states. For example, "split." will show diffs for both resulting goals. "all: swap 1 2" will show the same diffs as for the old proof state, though in a different position in the output. Please see comments before Proof_diffs.make_goal_map_i and Proof_diffs.match_goals for a description of how goals are matched between old and new proofs.
2018-07-29	Fix issue 8132. Print the content of body as in Printer.pr_compacted_decl,	Jim Fehrle
	not the type of body. Also update CHANGES to reflect that the argument for Set Diffs is a string.
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.