From a48cefa07907120c2270bf7a7689fa00a5adc167 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 7 Dec 2017 15:54:53 +0100 Subject: Fix anomaly in [Type foo] command, + print uctx like Check. --- test-suite/success/Check.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'test-suite') 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. -- cgit v1.2.3