From 239356d3a22af3b065dfae10bd6d84dd509251e8 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Tue, 3 Oct 2017 01:33:42 -0400
Subject: Add 8.7-only CacheTerm

---
 src/Util/Tactics/CacheTerm.v | 47 ++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 47 insertions(+)

(limited to 'src/Util/Tactics')

diff --git a/src/Util/Tactics/CacheTerm.v b/src/Util/Tactics/CacheTerm.v
index 4313a7f02..7541f907e 100644
--- a/src/Util/Tactics/CacheTerm.v
+++ b/src/Util/Tactics/CacheTerm.v
@@ -12,8 +12,55 @@ Ltac cache_term_with_type_by_gen ty abstract_tac id :=
                | _ => clear id'
                end in
   ret.
+Ltac cache_term_with_type_by ty tac id :=
+  cache_term_with_type_by_gen ty ltac:(fun id' => transparent_abstract tac using id') id.
 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_term_by tac id :=
+  let ty := open_constr:(_) in
+  cache_term_with_type_by ty tac id.
 Ltac cache_proof_by ty tac id :=
   let ty := open_constr:(_) in
   cache_proof_with_type_by ty tac id.
+Ltac cache_term term id :=
+  let ty := type of term in
+  cache_term_with_type_by ty ltac:(exact_no_check term) id.
+
+Ltac cache_sig_red_with_type_by ty tac red_tac red_cast_no_check id :=
+  let id' := fresh id in
+  let id' := fresh id in
+  let id' := cache_term_with_type_by ty tac id' in
+  let P := lazymatch ty with sig ?P => P end in
+  cache_term_with_type_by
+    ty
+    ltac:(let v := (eval cbv beta iota delta [id' proj1_sig] in (proj1_sig id')) in
+          let v := red_tac v in
+          (exists v);
+          abstract (
+              refine (eq_rect _ P (proj2_sig id') _ _);
+              red_cast_no_check (eq_refl v)
+            ))
+           id.
+Ltac cache_sig_red_with_type ty term red_tac red_cast_no_check id :=
+  let id' := fresh id in
+  let id' := fresh id in
+  let id' := cache_term term id' in
+  let P := lazymatch ty with sig ?P => P end in
+  cache_term_with_type_by
+    ty
+    ltac:(let v := (eval cbv beta iota delta [id' proj1_sig] in (proj1_sig id')) in
+          let v := red_tac v in
+          (exists v);
+          abstract (
+              refine (eq_rect _ P (proj2_sig id') _ _);
+              red_cast_no_check (eq_refl v)
+            ))
+           id.
+Ltac cache_sig_with_type_by ty tac id
+  := cache_sig_red_with_type_by ty tac ltac:(fun v => v) exact_no_check id.
+Ltac cache_vm_sig_with_type_by ty tac id
+  := cache_sig_red_with_type_by ty tac ltac:(fun v => eval vm_compute in v) vm_cast_no_check id.
+Ltac cache_sig_with_type ty term id
+  := cache_sig_red_with_type ty term ltac:(fun v => v) exact_no_check id.
+Ltac cache_vm_sig_with_type ty term id
+  := cache_sig_red_with_type ty term ltac:(fun v => eval vm_compute in v) vm_cast_no_check id.
-- 
cgit v1.2.3