1 files changed, 34 insertions, 0 deletions
diff --git a/contrib/subtac/Heq.v b/contrib/subtac/Heq.v
new file mode 100644
index 00000000..f2b216d9
--- /dev/null
+++ b/contrib/subtac/Heq.v
@@ -0,0 +1,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)).
+
+
+
+