diff options
Diffstat (limited to 'src/Util/Tactics/Revert.v')
| -rw-r--r-- | src/Util/Tactics/Revert.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Util/Tactics/Revert.v b/src/Util/Tactics/Revert.v index 5f549025d..78c94f956 100644 --- a/src/Util/Tactics/Revert.v +++ b/src/Util/Tactics/Revert.v @@ -3,8 +3,8 @@ Ltac revert_last_nondep := match goal with | [ H : _ |- _ ] => lazymatch goal with - | [ H' : appcontext[H] |- _ ] => fail - | [ |- appcontext[H] ] => fail + | [ H' : context[H] |- _ ] => fail + | [ |- context[H] ] => fail | _ => idtac end; revert H |