* Code simplification and clean-up. In particular there is no more code

  duplicated between add_relation and add_setoid.
* Less ad-hoc backward compatibility lemmas for setoids required in Setoid.v
* Term size reduction (first part): when a relation is registered, we add
  to the environment a definition that gives back either the relation as
  an argument or as a relation class. The definition is used to reduce
  the term size. [ Note: we could save a bit more by defining two definitions
  in place of one. However, we suppose that the lambda term fragments generated
  can be shared quite effectively. Thus we would recive almost no benefit by
  sharing in terms of size. What about proof checking time? ]


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6238 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 0 insertions, 26 deletions

diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v
index 2d48e82df..51703b23e 100644
--- a/theories/Setoids/Setoid.v
+++ b/theories/Setoids/Setoid.v
@@ -618,32 +618,6 @@ Record Setoid_Theory  (A: Type) (Aeq: relation A) : Prop :=
    Seq_sym : forall x y:A, Aeq x y -> Aeq y x;
    Seq_trans : forall x y z:A, Aeq x y -> Aeq y z -> Aeq x z}.
 
-Definition argument_class_of_setoid_theory:
- forall (A: Type) (Aeq: relation A),
-  Setoid_Theory Aeq -> Argument_Class.
- intros.
- apply (@SymmetricReflexive variance _ Aeq).
- exact (Seq_sym H).
- exact (Seq_refl H).
-Defined.
-
-Definition relation_class_of_setoid_theory :=
- fun A Aeq Setoid =>
-  relation_class_of_argument_class
-   (@argument_class_of_setoid_theory A Aeq Setoid).
-
-Definition equality_morphism_of_setoid_theory:
- forall (A: Type) (Aeq: relation A) (ST: Setoid_Theory Aeq),
-   let ASetoidClass := argument_class_of_setoid_theory ST in 
-    (Morphism_Theory (cons ASetoidClass (singl ASetoidClass))
-      Iff_Relation_Class).
- intros.
- exists Aeq.
- pose (sym   := Seq_sym ST);  clearbody sym.
- pose (trans := Seq_trans ST); clearbody trans.
- unfold make_compatibility_goal; simpl; split; eauto.
-Defined.
-
 (* END OF UTILITY/BACKWARD COMPATIBILITY PART *)
 
 (* A FEW EXAMPLES ON iff *)