diff options
| author | Hugo Herbelin | 2020-11-24 19:08:53 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-26 15:52:18 +0100 |
| commit | e353fe431351bb1f41bc6a8c813bea980e8d247c (patch) | |
| tree | 234b537d73fca9d5993804e0e5fae633397427dd /test-suite | |
| parent | 90cb2b0daf54cbd72c5ac8e1ffe2007c8901ddba (diff) | |
Fixes #13456: regression where tactic exists started to check evars incrementally.
The regression was due to #12365. We fix it by postponing the evars
check after the calls to the underlying constructor tactic, while
retaining using information from the first instantiations to resolve
the latter instantiations.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/bug_13456.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_13456.v b/test-suite/bugs/closed/bug_13456.v new file mode 100644 index 0000000000..b2e7fa7be5 --- /dev/null +++ b/test-suite/bugs/closed/bug_13456.v @@ -0,0 +1,5 @@ +Lemma minbug (n : nat) (P : nat -> Prop) (pn : P n) : exists (m : nat) (p : P m), True. +Proof. + exists _, pn. + exact I. +Qed. |