6 files changed, 64 insertions, 0 deletions
diff --git a/test-suite/misc/quick-include.sh b/test-suite/misc/quick-include.sh
new file mode 100755
index 0000000000..96bdee2fc2
--- /dev/null
+++ b/test-suite/misc/quick-include.sh
@@ -0,0 +1,5 @@
+#!/bin/sh
+set -e
+
+$coqc -R misc/quick-include/ QuickInclude -quick misc/quick-include/file1.v
+$coqc -R misc/quick-include/ QuickInclude -quick misc/quick-include/file2.v
diff --git a/test-suite/misc/quick-include/file1.v b/test-suite/misc/quick-include/file1.v
new file mode 100644
index 0000000000..fa48e240cb
--- /dev/null
+++ b/test-suite/misc/quick-include/file1.v
@@ -0,0 +1,18 @@
+
+Module Type E. End E.
+
+Module M.
+  Lemma x : True.
+  Proof. trivial. Qed.
+End M.
+
+
+Module Type T.
+  Lemma x : True.
+  Proof. trivial. Qed.
+End T.
+
+Module F(A:E).
+  Lemma x : True.
+  Proof. trivial. Qed.
+End F.
diff --git a/test-suite/misc/quick-include/file2.v b/test-suite/misc/quick-include/file2.v
new file mode 100644
index 0000000000..ab10dfd8de
--- /dev/null
+++ b/test-suite/misc/quick-include/file2.v
@@ -0,0 +1,6 @@
+
+From QuickInclude Require file1.
+
+Module M. Include file1.M. End M.
+Module T. Include file1.T. End T.
+Module F. Include file1.F. End F.
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index 46784d1897..d25ad5dca8 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -17,3 +17,7 @@ end
      : Expr -> Expr
 [(1 + 1)]
      : Expr
+Let "x" e1 e2
+     : expr
+Let "x" e1 e2
+     : expr
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 6bdbf1bed5..7800e91ee5 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -70,3 +70,27 @@ Notation "( x )" := x (in custom expr at level 0, x at level 2).
 Check [1 + 1].
 
 End C.
+
+(* An example of interaction between coercion and notations from
+   Robbert Krebbers. *)
+
+Require Import String.
+
+Module D.
+
+Inductive expr :=
+  | Var : string -> expr
+  | Lam : string -> expr -> expr
+  | App : expr -> expr -> expr.
+
+Notation Let x e1 e2 := (App (Lam x e2) e1).
+
+Parameter e1 e2 : expr.
+
+Check (Let "x" e1 e2).
+
+Coercion App : expr >-> Funclass.
+
+Check (Let "x" e1 e2).
+
+End D.
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 *)