aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Tactics/Contains.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Util/Tactics/Contains.v')
-rw-r--r--src/Util/Tactics/Contains.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/Util/Tactics/Contains.v b/src/Util/Tactics/Contains.v
index aa4fddac2..0ee6116e3 100644
--- a/src/Util/Tactics/Contains.v
+++ b/src/Util/Tactics/Contains.v
@@ -2,12 +2,12 @@
Ltac contains search_for in_term :=
idtac;
lazymatch in_term with
- | appcontext[search_for] => idtac
+ | context[search_for] => idtac
end.
Ltac free_in x y :=
idtac;
match y with
- | appcontext[x] => fail 1 x "appears in" y
+ | context[x] => fail 1 x "appears in" y
| _ => idtac
end.