Module mktac
Require
Import
CoqlibC
.
Ltac
cinv
H
:=
let
X
:=
fresh
in
set
(
X
:=
H
);
inv
X
.
Ltac
cset
H1
H2
:=
let
X
:=
fresh
in
set
(
X
:=
H2
);
eapply
H1
in
X
.
Ltac
cset2
H1
H2
:=
let
X
:=
fresh
in
set
(
X
:=
H1
);
specialize
(
X
H2
).