diff options
| author | Hugo Herbelin | 2020-05-10 21:48:34 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-05-13 12:13:15 +0200 |
| commit | 1e80f730590ba309b6eb1ae26832984fa7357761 (patch) | |
| tree | b663c20078deaef47dfb57ff7c112f321581163a /test-suite | |
| parent | 67f0e9fd40dc2f7b30a8aec4c7efb032e61a001e (diff) | |
Fixes #12233 (wrong printing env in presence of match branches eta-expansion).
At the same time, we propagate the correct binder relevance in detyping.
Note that this would be fixed by enforcing the context of branches in
the syntax of "Case".
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/bug_12233.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_12233.v b/test-suite/bugs/closed/bug_12233.v new file mode 100644 index 0000000000..3cbf084594 --- /dev/null +++ b/test-suite/bugs/closed/bug_12233.v @@ -0,0 +1,5 @@ +Theorem thm (A:Prop) (H:exists m:nat, True) : True. +destruct H as ([|],?). +assert A. +Show Proof. (* was raising Not_found since 8.7 *) +Abort. |