blob: 0ee6116e3b77c1a5a49a254a9ae28d5aff24457f (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
(** [contains x expr] succeeds iff [x] appears in [expr] *)
Ltac contains search_for in_term :=
idtac;
lazymatch in_term with
| context[search_for] => idtac
end.
Ltac free_in x y :=
idtac;
match y with
| context[x] => fail 1 x "appears in" y
| _ => idtac
end.
|