2 files changed, 25 insertions, 0 deletions
diff --git a/test-suite/prerequisite/make_local.v b/test-suite/prerequisite/make_local.v
new file mode 100644
index 00000000..8700a6c4
--- /dev/null
+++ b/test-suite/prerequisite/make_local.v
@@ -0,0 +1,10 @@
+(* Used in Import.v to test the locality flag *)
+
+Definition f (A:Type) (a:A) := a.
+
+Local Arguments Scope f [type_scope type_scope].
+Local Implicit Arguments f [A].
+
+(* Used in ImportedCoercion.v to test the locality flag *)
+
+Local Coercion g (b:bool) := if b then 0 else 1.
diff --git a/test-suite/prerequisite/make_notation.v b/test-suite/prerequisite/make_notation.v
new file mode 100644
index 00000000..3878e396
--- /dev/null
+++ b/test-suite/prerequisite/make_notation.v
@@ -0,0 +1,15 @@
+(* Used in Notation.v to test import of notations from files in sections *)
+
+Notation "'Z'" := O (at level 9).
+Notation plus := plus.
+Notation succ := S.
+Notation mult := mult (only parsing).
+Notation less := le (only parsing).
+
+(* Test bug 2168: ending section of some name was removing objects of the
+   same name *)
+
+Notation add2 n:=(S n).
+Section add2.
+End add2.
+