summaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/3684.v
blob: 94ce4a608f212e11b64c08ff377514f0d4e1266c (plain)
1
2
3
4
Definition foo : Set.
Proof.
  refine ($(abstract admit)$).
Qed.