Add break_innermost_match

1 files changed, 6 insertions, 0 deletions

diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v
index 2f9f6c59f..ea5d2e5e1 100644
--- a/src/Util/Tactics.v
+++ b/src/Util/Tactics.v
@@ -109,6 +109,12 @@ Ltac break_match_hyps_when_head_step T :=
                    constr_eq T T').
 Ltac break_match_when_head T := repeat break_match_when_head_step T.
 Ltac break_match_hyps_when_head T := repeat break_match_hyps_when_head_step T.
+Ltac break_innermost_match_step :=
+  break_match_step ltac:(fun v => lazymatch v with
+                                  | appcontext[match _ with _ => _ end] => fail
+                                  | _ => idtac
+                                  end).
+Ltac break_innermost_match := repeat break_innermost_match_step.
 
 Ltac free_in x y :=
   idtac;