diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-01-17 19:01:05 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-01-17 19:01:05 -0500 |
| commit | cb98e6d8a45b68e29546732a0eed969c724a0274 (patch) | |
| tree | 2a7511e9c051fd2050586edfd0da34392f5e02f9 /src/Util/Tactics | |
| parent | 31d802e9c11094d94c7ae7c13b05bd13639263fc (diff) | |
Fix infinite loop in destruct_rewrite_sumbool
Diffstat (limited to 'src/Util/Tactics')
| -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 |