diff options
Diffstat (limited to 'test-suite/bugs/closed/3372.v')
| -rw-r--r-- | test-suite/bugs/closed/3372.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3372.v b/test-suite/bugs/closed/3372.v new file mode 100644 index 00000000..91e3df76 --- /dev/null +++ b/test-suite/bugs/closed/3372.v @@ -0,0 +1,7 @@ +Set Universe Polymorphism. +Definition hProp : Type := sigT (fun _ : Type => True). +Goal Type. +Fail exact hProp@{Set}. (* test that it fails, but is not an anomaly *) +try (exact hProp@{Set}; fail 1). (* Toplevel input, characters 15-32: +Anomaly: Uncaught exception Invalid_argument("Array.iter2", _). +Please report. *) |