diff options
author | Jason Gross <jgross@mit.edu> | 2017-10-17 21:31:56 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-10-17 21:31:56 -0400 |
commit | befc9c3c404ece31e3eb9d7715ee694395bd5fb5 (patch) | |
tree | a4208a853fa1006abe7186c6cf3e2c82909ff18d /src | |
parent | e8bb3c232fd41aba3c7bf8ea6387e062abaf93fc (diff) |
Add CacheTerm
The real use of this is with the 8.7-only transparent_abstract, but we
can do some things even when we can only cache proofs.
Diffstat (limited to 'src')
-rw-r--r-- | src/Util/Tactics.v | 1 | ||||
-rw-r--r-- | src/Util/Tactics/CacheTerm.v | 19 |
2 files changed, 20 insertions, 0 deletions
diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index 3cd86b0c3..5a2bca803 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -1,6 +1,7 @@ (** * Generic Tactics *) Require Export Crypto.Util.FixCoqMistakes. Require Export Crypto.Util.Tactics.BreakMatch. +Require Export Crypto.Util.Tactics.CacheTerm. Require Export Crypto.Util.Tactics.ChangeInAll. Require Export Crypto.Util.Tactics.ClearAll. Require Export Crypto.Util.Tactics.ClearDuplicates. 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. |