diff options
| -rw-r--r-- | src/Util/Tactics/BreakMatch.v | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/Util/Tactics/BreakMatch.v b/src/Util/Tactics/BreakMatch.v index 5ad882c6f..486d3ef92 100644 --- a/src/Util/Tactics/BreakMatch.v +++ b/src/Util/Tactics/BreakMatch.v @@ -53,7 +53,11 @@ Ltac destruct_rewrite_sumbool e := destruct e as [H|H]; try lazymatch type of H with | ?LHS = ?RHS - => rewrite ?H; rewrite ?H in *; + => lazymatch RHS with + | context[LHS] => fail + | _ => idtac + end; + rewrite ?H; rewrite ?H in *; repeat match goal with | [ |- context G[LHS] ] => let LHS' := fresh in |