From d5298f223b503d8ca02c6869ba269bf8f4b84b96 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sun, 28 Oct 2018 14:43:11 -0400
Subject: Improve cps_id tactics, add add_var_types_cps_id,
 unify_extracted_cps_id tactics

---
 src/Util/Tactics/CPSId.v | 45 +++++++++++++++++++++++++--------------------
 1 file changed, 25 insertions(+), 20 deletions(-)

(limited to 'src/Util')

diff --git a/src/Util/Tactics/CPSId.v b/src/Util/Tactics/CPSId.v
index 076eed95a..92b694396 100644
--- a/src/Util/Tactics/CPSId.v
+++ b/src/Util/Tactics/CPSId.v
@@ -16,26 +16,31 @@ Ltac ensure_complex_continuation allow_option k :=
        end
   end.
 
-Ltac cps_id_step allow_option match_to_cont_lem :=
-  match goal with
-  | [ |- context[?e] ]
-    => let res := match_to_cont_lem e in
-       lazymatch res with
-       | (?k, ?lem)
-         => ensure_complex_continuation allow_option k;
-            (* sometimes reduction mismatches happen, so we cast [lem] to fix them *)
-            (rewrite lem || rewrite (lem : e = _))
-       end
-  | [ H : context[?e] |- _ ]
-    => let res := match_to_cont_lem e in
-       lazymatch res with
-       | (?k, ?lem)
-         => ensure_complex_continuation allow_option k;
-            (* sometimes reduction mismatches happen, so we cast [lem] to fix them *)
-            (rewrite lem in H || rewrite (lem : e = _) in H)
+Ltac cps_id_step allow_option lem :=
+  let lem := open_constr:(lem) in
+  lazymatch type of lem with
+  | ?T -> _ => cps_id_step allow_option open_constr:(lem _)
+  | ?lhs = ?k ?rhs
+    => match goal with
+       | [ |- context[?e] ]
+         => (* take advantage of lazymatch treating evars as holes/wildcards *)
+         lazymatch e with
+         | lhs
+           => let lem := constr:(lem : e = _) in
+              ensure_complex_continuation allow_option k;
+              rewrite lem
+         end
+       | [ H : context[?e] |- _ ]
+         => (* take advantage of lazymatch treating evars as holes/wildcards *)
+         lazymatch e with
+         | lhs
+           => let lem := constr:(lem : e = _) in
+              ensure_complex_continuation allow_option k;
+              rewrite lem in H
+         end
        end
   end.
 
-Ltac cps_id allow_option match_to_cont_lem := repeat cps_id_step allow_option match_to_cont_lem.
-Ltac cps_id_with_option match_to_cont_lem := cps_id true match_to_cont_lem.
-Ltac cps_id_no_option match_to_cont_lem := cps_id false match_to_cont_lem.
+Ltac cps_id allow_option lem := repeat cps_id_step allow_option lem.
+Tactic Notation "cps_id_with_option" uconstr(lem) := cps_id true lem.
+Tactic Notation "cps_id_no_option" uconstr(lem) := cps_id false lem.
-- 
cgit v1.2.3