Improve cps_id tactics, add add_var_types_cps_id, unify_extracted_cps_id tactics

1 files changed, 25 insertions, 20 deletions

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.