From a7121ed7ba1a5a55845b5ffa4846b8aa0e293e5d Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Wed, 7 Nov 2018 00:23:07 -0800
Subject: 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

---
 test-suite/unit-tests/printing/proof_diffs_test.ml | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/unit-tests/printing/proof_diffs_test.ml b/test-suite/unit-tests/printing/proof_diffs_test.ml
index 526cefec44..7f9e6cc6e0 100644
--- a/test-suite/unit-tests/printing/proof_diffs_test.ml
+++ b/test-suite/unit-tests/printing/proof_diffs_test.ml
@@ -71,6 +71,13 @@ let _ = add_test "tokenize_string examples" t
 
 open Pp
 
+(* example that was failing from #8922 *)
+let t () =
+  Proof_diffs.write_diffs_option "removed";
+  ignore (diff_str "X : ?Goal" "X : forall x : ?Goal0, ?Goal1");
+  Proof_diffs.write_diffs_option "on"
+let _ = add_test "shorten_diff_span failure from #8922" t
+
 (* note pp_to_string concatenates adjacent strings, could become one token,
 e.g. str " a" ++ str "b " will give a token "ab" *)
 (* checks background is present and correct *)
-- 
cgit v1.2.3