blob: 4313a7f02407e2e011fec11ab91924a0eaa258f1 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
Require Import Crypto.Util.Tactics.TransparentAssert.
Ltac cache_term_with_type_by_gen ty abstract_tac id :=
let id' := fresh id in
let dummy := match goal with
| _ => transparent assert ( id' : ty );
[ abstract_tac id'
| ]
end in
let ret := (eval cbv [id'] in id') in
let dummy := match goal with
| _ => clear id'
end in
ret.
Ltac cache_proof_with_type_by ty tac id :=
cache_term_with_type_by_gen ty ltac:(fun id' => abstract tac using id') id.
Ltac cache_proof_by ty tac id :=
let ty := open_constr:(_) in
cache_proof_with_type_by ty tac id.
|
