1 2 3 4 5
Require Import TestSuite.admit. Definition foo : Set. Proof. refine (ltac:(abstract admit)). Qed.