3 files changed, 19 insertions, 0 deletions
diff --git a/test-suite/output/PrintUnivsSubgraph.out b/test-suite/output/PrintUnivsSubgraph.out
new file mode 100644
index 0000000000..c42e15e4e8
--- /dev/null
+++ b/test-suite/output/PrintUnivsSubgraph.out
@@ -0,0 +1,5 @@
+Prop < Set
+Set < i
+    < j
+i < j
+
diff --git a/test-suite/output/PrintUnivsSubgraph.v b/test-suite/output/PrintUnivsSubgraph.v
new file mode 100644
index 0000000000..ec9cf44d4f
--- /dev/null
+++ b/test-suite/output/PrintUnivsSubgraph.v
@@ -0,0 +1,9 @@
+
+Universes i j k l.
+
+Definition foo : Type@{j} := Type@{i}.
+
+Definition baz : Type@{k} := Type@{l}.
+
+Print Universes Subgraph(i j).
+(* should print [i < j], not [l < k] (and not prelude universes) *)
diff --git a/test-suite/success/Require.v b/test-suite/success/Require.v
index f851d8c7d9..de5987c4f7 100644
--- a/test-suite/success/Require.v
+++ b/test-suite/success/Require.v
@@ -1,3 +1,8 @@
+(* -*- coq-prog-args: ("-noinit"); -*- *)
+
 Require Import Coq.Arith.Plus.
 Require Coq.Arith.Minus.
 Locate Library Coq.Arith.Minus.
+
+(* Check that Init didn't get exported by the import above *)
+Fail Check nat.