aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/Util/Tactics.v32
1 files changed, 32 insertions, 0 deletions
diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v
index ea5d2e5e1..128fdcfd0 100644
--- a/src/Util/Tactics.v
+++ b/src/Util/Tactics.v
@@ -487,3 +487,35 @@ Ltac idtac_context :=
idtac_goal;
lazymatch goal with |- ?G => idtac "Context:" G end;
fail).
+
+(** Destruct the convoy pattern ([match e as x return x = e -> _ with _ => _ end eq_refl] *)
+Ltac convoy_destruct_gen T change_in :=
+ let e' := fresh in
+ let H' := fresh in
+ match T with
+ | context G[?f eq_refl]
+ => match f with
+ | match ?e with _ => _ end
+ => pose e as e';
+ match f with
+ | context F[e]
+ => let F' := context F[e'] in
+ first [ pose (eq_refl : e = e') as H';
+ let G' := context G[F' H'] in
+ change_in G';
+ clearbody H' e'
+ | pose (eq_refl : e' = e) as H';
+ let G' := context G[F' H'] in
+ change_in G';
+ clearbody H' e' ]
+ end
+ end;
+ destruct e'
+ end.
+
+Ltac convoy_destruct_in H :=
+ let T := type of H in
+ convoy_destruct_gen T ltac:(fun T' => change T' in H).
+Ltac convoy_destruct :=
+ let T := get_goal in
+ convoy_destruct_gen T ltac:(fun T' => change T').