diff options
Diffstat (limited to 'src/Util/Tactics/Contains.v')
-rw-r--r-- | src/Util/Tactics/Contains.v | 4 |
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. |