diff options
Diffstat (limited to 'src/Util/Tactics/CacheTerm.v')
-rw-r--r-- | src/Util/Tactics/CacheTerm.v | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/src/Util/Tactics/CacheTerm.v b/src/Util/Tactics/CacheTerm.v new file mode 100644 index 000000000..4313a7f02 --- /dev/null +++ b/src/Util/Tactics/CacheTerm.v @@ -0,0 +1,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. |