diff options
author | Jason Gross <jgross@mit.edu> | 2016-10-30 19:21:46 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2016-10-30 19:21:46 -0400 |
commit | 6936dba302a6b9429dfc054e8b5df3b1174d6d5e (patch) | |
tree | 304485459c4014b5e1cb1f9f6108d4966a6d9683 /src/Util | |
parent | 3fbd49b8905cf97e955a6aacdc59913f65c56c5e (diff) |
Add break_innermost_match
Diffstat (limited to 'src/Util')
-rw-r--r-- | src/Util/Tactics.v | 6 |
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; |