aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-12-13 23:54:09 +0100
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-12-13 23:54:09 +0100
commitb1aaedb9e728702cccdb1bd126a714d9e075d14c (patch)
treea002f33d402eceefc9451ac434825f71d3712f2d /test-suite
parent2a4bf4764b61e7d7fddb05b504360814de441ba9 (diff)
parenta48cefa07907120c2270bf7a7689fa00a5adc167 (diff)
Merge PR #6341: Fix anomaly in [Type foo] command, + print uctx like Check.
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/success/Check.v2
1 files changed, 2 insertions, 0 deletions
diff --git a/test-suite/success/Check.v b/test-suite/success/Check.v
index 0f677a849..82b51b1ff 100644
--- a/test-suite/success/Check.v
+++ b/test-suite/success/Check.v
@@ -12,3 +12,5 @@
Check 0.
Check S.
Check nat.
+
+Type Type : Type.