aboutsummaryrefslogtreecommitdiff
path: root/printing/proof_diffs.mli
diff options
context:
space:
mode:
Diffstat (limited to 'printing/proof_diffs.mli')
-rw-r--r--printing/proof_diffs.mli6
1 files changed, 6 insertions, 0 deletions
diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli
index ea64439456..6bdd7004fb 100644
--- a/printing/proof_diffs.mli
+++ b/printing/proof_diffs.mli
@@ -25,6 +25,10 @@ val write_color_enabled : bool -> unit
(** true indicates that color output is enabled *)
val color_enabled : unit -> bool
+type diffOpt = DiffOff | DiffOn | DiffRemoved
+
+val string_to_diffs : string -> diffOpt
+
open Evd
open Environ
open Constr
@@ -84,3 +88,5 @@ type hyp_info = {
}
val diff_hyps : string list list -> hyp_info CString.Map.t -> string list list -> hyp_info CString.Map.t -> Pp.t list
+
+val diff_proofs : diff_opt:diffOpt -> ?old:Proof.t -> Proof.t -> Pp.t