Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

1 files changed, 0 insertions, 34 deletions

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