diff options
| author | Pierre-Marie Pédrot | 2020-10-15 15:14:23 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-10-15 15:14:23 +0200 |
| commit | 4bf43453ec5f635ae87a2edeb4f51d95f2d5ac67 (patch) | |
| tree | ce78494f5923cdde51c7a3ba4acf0133b1640bfe /test-suite | |
| parent | fc0ee016b2bbffd73c5a9aa7784f2c255f80d39d (diff) | |
| parent | 34e1aeef7718dd3042ef22cd1ded9d9eb65cfd87 (diff) | |
Merge PR #13181: Guard unify_leq_delay calls in Typing
Reviewed-by: ppedrot
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/bug_13171.v | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_13171.v b/test-suite/bugs/closed/bug_13171.v new file mode 100644 index 0000000000..0564722729 --- /dev/null +++ b/test-suite/bugs/closed/bug_13171.v @@ -0,0 +1,10 @@ +Primitive array := #array_type. + +Goal False. +Proof. + unshelve epose (_:nat). exact_no_check true. + Fail let c := open_constr:([| n | 0 |]) in + let c := eval cbv in c in + let c := type of c in + idtac c. +Abort. |