diff options
Diffstat (limited to 'test-suite/success/unshelve.v')
| -rw-r--r-- | test-suite/success/unshelve.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/success/unshelve.v b/test-suite/success/unshelve.v index 672222bd..a4fa544c 100644 --- a/test-suite/success/unshelve.v +++ b/test-suite/success/unshelve.v @@ -9,3 +9,11 @@ unshelve (refine (F _ _ _ _)). + exact (@eq_refl bool true). + exact (@eq_refl unit tt). Qed. + +(* This was failing in 8.6, because of ?a:nat being wrongly duplicated *) + +Goal (forall a : nat, a = 0 -> True) -> True. +intros F. +unshelve (eapply (F _);clear F). +2:reflexivity. +Qed. |