aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/misc/universes.sh
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite/misc/universes.sh')
-rwxr-xr-xtest-suite/misc/universes.sh8
1 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/misc/universes.sh b/test-suite/misc/universes.sh
new file mode 100755
index 000000000..d87a86035
--- /dev/null
+++ b/test-suite/misc/universes.sh
@@ -0,0 +1,8 @@
+# Sort universes for the whole standard library
+EXPECTED_UNIVERSES=4 # Prop is not counted
+$coqc -R misc/universes Universes misc/universes/all_stdlib 2>&1
+$coqc -R misc/universes Universes misc/universes/universes 2>&1
+mv universes.txt misc/universes
+N=`awk '{print $3}' misc/universes/universes.txt | sort -u | wc -l`
+printf "Found %s/%s universes\n" $N $EXPECTED_UNIVERSES
+if [ "$N" -eq $EXPECTED_UNIVERSES ]; then exit 0; else exit 1; fi