diff options
Diffstat (limited to 'src/Util/Tactics/BreakMatch.v')
| -rw-r--r-- | src/Util/Tactics/BreakMatch.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/Util/Tactics/BreakMatch.v b/src/Util/Tactics/BreakMatch.v index 486d3ef92..f03823a92 100644 --- a/src/Util/Tactics/BreakMatch.v +++ b/src/Util/Tactics/BreakMatch.v @@ -117,4 +117,10 @@ Ltac break_innermost_match_step := | appcontext[match _ with _ => _ end] => fail | _ => idtac end). +Ltac break_innermost_match_hyps_step := + break_match_hyps_step ltac:(fun v => lazymatch v with + | appcontext[match _ with _ => _ end] => fail + | _ => idtac + end). Ltac break_innermost_match := repeat break_innermost_match_step. +Ltac break_innermost_match_hyps := repeat break_innermost_match_hyps_step. |