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.

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.