blob: f2b216d9608bb605c1af8825a41989986a7f03be (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
|
Require Export JMeq.
(** Notation for heterogenous equality. *)
Notation " [ x : X ] = [ y : Y ] " := (@JMeq X x Y y) (at level 0, X at next level, Y at next level).
(** Do something on an heterogeneous equality appearing in the context. *)
Ltac on_JMeq tac :=
match goal with
| [ H : @JMeq ?x ?X ?y ?Y |- _ ] => tac H
end.
(** Try to apply [JMeq_eq] to get back a regular equality when the two types are equal. *)
Ltac simpl_one_JMeq :=
on_JMeq
ltac:(fun H => let H' := fresh "H" in
assert (H' := JMeq_eq H) ; clear H ; rename H' into H).
(** Repeat it for every possible hypothesis. *)
Ltac simpl_JMeq := repeat simpl_one_JMeq.
(** Just simplify an h.eq. without clearing it. *)
Ltac simpl_one_dep_JMeq :=
on_JMeq
ltac:(fun H => let H' := fresh "H" in
assert (H' := JMeq_eq H)).
|
