aboutsummaryrefslogtreecommitdiff
path: root/printing/proof_diffs.ml
AgeCommit message (Expand)Author
2020-06-29Moving the remaining Refiner functions to Tacmach.Pierre-Marie Pédrot
2020-04-06Clean and fix definitions of options.Théo Zimmermann
2020-03-31Merge PR #11647: [rfc] Consolidation of parsing interfacesPierre-Marie Pédrot
2020-03-30Merge PR #11817: [cleanup] Remove unnecessary Map/Set module creationGaëtan Gilbert
2020-03-25[parsing] Move `coq_parsable` custom logic to Grammar.Emilio Jesus Gallego Arias
2020-03-19Merge PR #11795: Print implicit arguments in types of referencesHugo Herbelin
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-13[cleanup] Remove unnecessary Map/Set module creationEmilio Jesus Gallego Arias
2020-03-12Print implicit arguments in types of referencesSimonBoulier
2020-02-19Addressing #6082 and #7766 (overriding format of notation).Hugo Herbelin
2020-02-12Remove Goptions.opt_name fieldGaëtan Gilbert
2019-12-06Moving the diversity of constr printers to a label style.Hugo Herbelin
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-23Fixing typos - Part 3JPR
2019-04-16Clean the representation of recursive annotation in ConstrexprMaxime Dénès
2019-03-31Multiple payload types in tokensPierre Roux
2019-03-27[printing] Removal of imperative state.Emilio Jesus Gallego Arias
2019-03-20Stop accessing proof env via Pfedit in printersMaxime Dénès
2019-03-20Merge PR #8669: Show diffs in some error messagesEmilio Jesus Gallego Arias
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-02-28Show diffs in error messages if color is enabledJim Fehrle
2019-01-06Renaming pr_evar_suggested_name into -> evar_suggested_name.Hugo Herbelin
2018-12-20Make diffs work for more input stringsJim Fehrle
2018-12-14[proof] Rework proof interface.Emilio Jesus Gallego Arias
2018-12-10Fix Invalid_argument in List.iter2Jim Fehrle
2018-12-10For diffs, return exactly the characters that make up STRING and FIELD tokensJim Fehrle
2018-12-10Fix #9091: don't show deleted compacted hypotheses twice in diffJim Fehrle
2018-12-10Treat unmatched goals as new for diffs (highlighted)Jim Fehrle
2018-11-23s/let _ =/let () =/ in some places (mostly goptions related)Gaëtan Gilbert
2018-11-22Merge PR #8967: Fix #8922 (uncaught pp_diff exception)Hugo Herbelin
2018-11-21[gramlib] [build] Switch make-based system to packed gramlibEmilio Jesus Gallego Arias
2018-11-14Get hyps and goal the same way Printer does; don't omit infoJim Fehrle
2018-10-02Revert #6651: Use r.(p) syntax to print primitive projectionsMaxime Dénès
2018-09-20Current diff code only compares the first current goal of the old and newJim Fehrle
2018-07-29Fix issue 8132. Print the content of body as in Printer.pr_compacted_decl,Jim Fehrle
2018-07-23Make tokenize_string an optional parameter for diff methods in pp_diffs.Jim Fehrle
2018-07-23Displays the differences between successive proof steps in coqtop and CoqIDE.Jim Fehrle
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:57:49 +0000