diff options
Diffstat (limited to 'contrib/subtac/Heq.v')
| -rw-r--r-- | contrib/subtac/Heq.v | 34 |
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)). - - - - |