coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of lib/pp_diff.ml

October 2024

coqbot-app[bot]
Merge PR #19692: Update the OCaml headers to reflect the fact Coq is now Rocq.
committed
Pierre-Marie Pédrot
Update the OCaml headers to reflect the fact Coq is now Rocq.
committed

November 2021

coqbot-app[bot]
Merge PR #15132: Fix #14577: always include every new line ident when diffing hypothesis lines
committed
Jim Fehrle
Minor cleanup
committed

June 2021

Pierre-Marie Pédrot
Merge PR #14457: Show a warning instead of an anomaly for Diff_Failure exception
committed
Jim Fehrle
Print a message instead of an anomaly for Diff_Failure exception
committed

October 2020

coqbot-app[bot]
Merge PR #12874: Add a "Show Proof Diffs" message to the XML protocol
committed
Jim Fehrle
Add an XML message for "Show Proof Diffs" Add menu item that uses this
committed

March 2020

Hugo Herbelin
Merge PR #11559: Remove year in headers.
committed
Théo Zimmermann
Update headers in the whole code base.
committed

June 2019

Clément Pit-Claudel
Merge PR #10320: Update headers to the new year.
committed
Théo Zimmermann
Update ml-style headers to new year.
committed

November 2018

Hugo Herbelin
Merge PR #8967: Fix #8922 (uncaught pp_diff exception)
committed
Jim Fehrle
Get hyps and goal the same way Printer does; don't omit info Allow for new goals that don't map to old goals Include background_goals in all_goals return value Fix incorrect change to raw diffs in shorten_diff_span Fixes #8922
committed

July 2018

Emilio Jesus Gallego Arias
Merge PR #6801: Highlight differences between successive proof steps (color, underline, etc.)
committed
Jim Fehrle
Make tokenize_string an optional parameter for diff methods in pp_diffs. Remove forward reference to lexer.
committed
Jim Fehrle
Displays the differences between successive proof steps in coqtop and CoqIDE. Proof General requires minor changes to make the diffs visible, but this code shouldn't break the existing version of PG.
committed