aboutsummaryrefslogtreecommitdiff
path: root/printing/proof_diffs.mli
diff options
context:
space:
mode:
authorJim Fehrle2019-07-06 19:25:39 -0700
committerJim Fehrle2019-10-29 11:25:01 -0700
commit5ec7eca640a6ee495eb2c0fb8d8a4076256ff96d (patch)
tree31fa1c193537525928905d9f22b93b91b4ed1a00 /printing/proof_diffs.mli
parentf508ddcd2cfff152b8d6291d96e4b87ef9fe2ff9 (diff)
Show diffs in "Show Proof."
Add experimental "Show Proof" command to the toplevel that shadows the current command in the parser (in coqtop and PG only). Apply existing code to highlight diffs in the output
Diffstat (limited to 'printing/proof_diffs.mli')
-rw-r--r--printing/proof_diffs.mli3
1 files changed, 3 insertions, 0 deletions
diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli
index f6fca91eea..a806ab7123 100644
--- a/printing/proof_diffs.mli
+++ b/printing/proof_diffs.mli
@@ -16,6 +16,9 @@ val write_diffs_option : string -> unit
(** Returns true if the diffs option is "on" or "removed" *)
val show_diffs : unit -> bool
+(** Returns true if the diffs option is "removed" *)
+val show_removed : unit -> bool
+
(** controls whether color output is enabled *)
val write_color_enabled : bool -> unit