diff options
Diffstat (limited to 'test-suite/bugs/closed/5036.v')
| -rw-r--r-- | test-suite/bugs/closed/5036.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/5036.v b/test-suite/bugs/closed/5036.v index 12c958be..83f16774 100644 --- a/test-suite/bugs/closed/5036.v +++ b/test-suite/bugs/closed/5036.v @@ -7,4 +7,4 @@ Section foo. autorewrite with core. constructor. Qed. -End foo. (* Anomaly: Universe Top.16 undefined. Please report. *)
\ No newline at end of file +End foo. (* Anomaly: Universe Top.16 undefined. Please report. *) |