5 files changed, 57 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.