diff options
| -rw-r--r-- | _CoqProject | 1 | ||||
| -rw-r--r-- | src/Util/Tactics.v | 1 | ||||
| -rw-r--r-- | src/Util/Tactics/CacheTerm.v | 19 |
3 files changed, 21 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject index 91ca74ade..a1c7babdc 100644 --- a/_CoqProject +++ b/_CoqProject @@ -341,6 +341,7 @@ src/Util/Sigma/Associativity.v src/Util/Sigma/Lift.v src/Util/Sigma/MapProjections.v src/Util/Tactics/BreakMatch.v +src/Util/Tactics/CacheTerm.v src/Util/Tactics/ChangeInAll.v src/Util/Tactics/ClearAll.v src/Util/Tactics/ClearDuplicates.v 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. |