Revert "Add more instances for type.related"

This reverts commit 68c4b1ad628b82503e674aa42435d1d4bfbcbe3f.

I think it was making things too slow.

1 files changed, 4 insertions, 15 deletions

diff --git a/src/Experiments/NewPipeline/LanguageWf.v b/src/Experiments/NewPipeline/LanguageWf.v
index b5a62687c..9c1c24a22 100644
--- a/src/Experiments/NewPipeline/LanguageWf.v
+++ b/src/Experiments/NewPipeline/LanguageWf.v
@@ -38,28 +38,17 @@ Module Compilers.
       Context {base_type} {interp_base_type : base_type -> Type}.
       Local Notation eqv := (@type.related base_type interp_base_type (fun _ => eq)).
 
-      Global Instance related_Symmetric {t} {R : forall t, relation (interp_base_type t)}
-             {R_sym : forall t, Symmetric (R t)}
-        : Symmetric (@type.related base_type interp_base_type R t) | 10.
-      Proof.
-        cbv [Symmetric] in *;
-          induction t; cbn [type.related type.interp] in *; repeat intro; eauto.
-      Qed.
+      Global Instance eqv_Symmetric {t} : Symmetric (@eqv t) | 10.
+      Proof. induction t; cbn [type.eqv type.interp] in *; repeat intro; eauto. Qed.
 
-      Global Instance related_Transitive {t} {R : forall t, relation (interp_base_type t)}
-             {R_sym : forall t, Symmetric (R t)}
-             {R_trans : forall t, Transitive (R t)}
-        : Transitive (@type.related base_type interp_base_type R t) | 10.
+      Global Instance eqv_Transitive {t} : Transitive (@eqv t) | 10.
       Proof.
-        induction t; cbn [type.related]; [ exact _ | ].
+        induction t; cbn [eqv]; [ exact _ | ].
         cbv [respectful]; cbn [type.interp].
         intros f g h Hfg Hgh x y Hxy.
         etransitivity; [ eapply Hfg; eassumption | eapply Hgh ].
         etransitivity; first [ eassumption | symmetry; eassumption ].
       Qed.
-
-      Global Instance eqv_Transitive {t} : Transitive (@eqv t) | 10 := _.
-      Global Instance eqv_Symmetric {t} : Symmetric (@eqv t) | 10 := _.
     End eqv.
 
     Section app_curried_instances.