From befc9c3c404ece31e3eb9d7715ee694395bd5fb5 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 17 Oct 2017 21:31:56 -0400 Subject: 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. --- src/Util/Tactics/CacheTerm.v | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 src/Util/Tactics/CacheTerm.v (limited to 'src/Util/Tactics') 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. -- cgit v1.2.3