blob: 1a774bdfc5f407548177c402f93ceae4eaac56ac (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
Ltac print_context _ :=
lazymatch goal with
| [ H : ?T |- False ]
=> try ((clear H || fail 10000 "Anomaly in print_context: could not clear" H); print_context (); fail);
match goal with
| _ => let body := (eval cbv delta [H] in H) in
idtac H ":=" body ":" T
| _ => idtac H ":" T
end
| [ |- False ] => idtac
| [ |- _ ] => try (exfalso; print_context (); fail)
end.
|
