diff options
| author | Hugo Herbelin | 2018-11-22 10:56:06 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2018-11-22 10:56:06 +0100 |
| commit | 2d0be200ab9a2e3a0ff7b383078aabe70f24dd82 (patch) | |
| tree | bd9618861bd9d0ed11ee1e52c36340a2a7b9eed8 /test-suite/unit-tests | |
| parent | ba646509c8946dfa513c30e9b9659643af798cf3 (diff) | |
| parent | a7121ed7ba1a5a55845b5ffa4846b8aa0e293e5d (diff) | |
Merge PR #8967: Fix #8922 (uncaught pp_diff exception)
Diffstat (limited to 'test-suite/unit-tests')
| -rw-r--r-- | test-suite/unit-tests/printing/proof_diffs_test.ml | 7 |
1 files changed, 7 insertions, 0 deletions
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 *) |