blob: eb3c4f4b9c7c7416f5ca3828f50b812fb407238b (
plain)
1
2
3
4
5
6
7
8
9
|
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.
|
