From 6133c0633f4a3545de4017325d0f213fbbb5c07d Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Mon, 10 Sep 2018 18:06:33 +0200
Subject: Print Universes Subgraph

This adds an optional [Subgraph] part to the Print Universes command,
eg [Print Universes Subgraph(i j)] to print only constraints related
to i and j (and Prop/Set).
---
 test-suite/output/PrintUnivsSubgraph.out | 5 +++++
 test-suite/output/PrintUnivsSubgraph.v   | 9 +++++++++
 2 files changed, 14 insertions(+)
 create mode 100644 test-suite/output/PrintUnivsSubgraph.out
 create mode 100644 test-suite/output/PrintUnivsSubgraph.v

(limited to 'test-suite')

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) *)
-- 
cgit v1.2.3