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.mli9
1 files changed, 1 insertions, 8 deletions
diff --git a/printing/proof_diffs.mli b/printing/proof_diffs.mli
index 83e721d3d5..24b171770a 100644
--- a/printing/proof_diffs.mli
+++ b/printing/proof_diffs.mli
@@ -83,11 +83,4 @@ type hyp_info = {
mutable done_: bool;
}
-module StringMap :
-sig
- type +'a t
- val empty: hyp_info t
- val add : string -> hyp_info -> hyp_info t -> hyp_info t
-end
-
-val diff_hyps : string list list -> hyp_info StringMap.t -> string list list -> hyp_info StringMap.t -> Pp.t list
+val diff_hyps : string list list -> hyp_info CString.Map.t -> string list list -> hyp_info CString.Map.t -> Pp.t list