aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/unshelve.v
blob: 672222bdd641f31483ddac3fc38eb86f02961165 (plain)
1
2
3
4
5
6
7
8
9
10
11
Axiom F : forall (b : bool), b = true ->
  forall (i : unit), i = i -> True.

Goal True.
Proof.
unshelve (refine (F _ _ _ _)).
+ exact true.
+ exact tt.
+ exact (@eq_refl bool true).
+ exact (@eq_refl unit tt).
Qed.