blob: f4e405de72b8d40be2147556467ebd7716c6c32d (
plain)
1
2
3
4
5
6
7
8
9
10
|
Tactic Notation "basicapply" open_constr(R) "using" tactic3(tac) "sideconditions" tactic0(tacfin) := idtac.
Tactic Notation "basicapply" open_constr(R) := basicapply R using (fun Hlem => idtac) sideconditions (autounfold with spred; idtac).
(* segfault in coqtop *)
Tactic Notation "basicapply" tactic0(tacfin) := idtac.
Goal True.
basicapply subst.
Abort.
|
