blob: c180559628bd8b618236387b79cbd8337fb92165 (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
(** Work around "Cannot create self-referring hypothesis" coming from
[change x with y in *] *)
Ltac change_in_all from to :=
change from with to;
repeat match goal with
| [ H : _ |- _ ] => progress change from with to in H
end.
Ltac change_with_compute_in_all c :=
let c' := (eval compute in c) in
change c with c' in *.
|
