diff options
Diffstat (limited to 'test-suite/bugs/closed/HoTT_coq_059.v')
| -rw-r--r-- | test-suite/bugs/closed/HoTT_coq_059.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_059.v b/test-suite/bugs/closed/HoTT_coq_059.v index 2e6c735cf5..9800ba8e45 100644 --- a/test-suite/bugs/closed/HoTT_coq_059.v +++ b/test-suite/bugs/closed/HoTT_coq_059.v @@ -15,3 +15,4 @@ Section foo. (* Toplevel input, characters 0-60: Error: Universe inconsistency (cannot enforce Top.24 <= Top.23 because Top.23 < Top.22 <= Top.24). *) +End foo. |