-(* FOR BACKWARD COMPATIBILITY *)
-Implicit Arguments Setoid_Theory [].
-Implicit Arguments Seq_refl [].
-Implicit Arguments Seq_sym [].
-Implicit Arguments Seq_trans [].
-
-
-(* Some tactics for manipulating Setoid Theory not officially
- declared as Setoid. *)
-
-Ltac trans_st x := match goal with
- | H : Setoid_Theory ? ?eqA |- ?eqA ? ? =>
- apply (Seq_trans ? ? H) with x; auto
- end.
-
-Ltac sym_st := match goal with
- | H : Setoid_Theory ? ?eqA |- ?eqA ? ? =>
- apply (Seq_sym ? ? H); auto
- end.
-
-Ltac refl_st := match goal with
- | H : Setoid_Theory ? ?eqA |- ?eqA ? ? =>
- apply (Seq_refl ? ? H); auto
- end.
-
-definition gen_st : ∀A : Set. Setoid_Theory ? (@eq A).
-Proof. constructor; congruence. Qed.
-