Fix the clrewrite tactic, change Relations.v to work on relations in Prop

only, and get rid of the "relation" definition which makes unification
fail blatantly. Replace it with a notation :) In its current state,
the new tactic seems ready for larger tests.


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

1 files changed, 9 insertions, 5 deletions

diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index 5e18ef2af..8c8c8c67c 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -31,9 +31,10 @@ Class Setoid A :=
   equiv : relation A ;
   setoid_equiv :> Equivalence A equiv.
 
-Program Instance [ eqa : Equivalence A (eqA : relation A) ] => 
-  equivalence_setoid : Setoid A :=
-  equiv := eqA ; setoid_equiv := eqa.
+(* Too dangerous instance *)
+(* Program Instance [ eqa : Equivalence A eqA ] =>  *)
+(*   equivalence_setoid : Setoid A := *)
+(*   equiv := eqA ; setoid_equiv := eqa. *)
 
 (** Shortcuts to make proof search easier. *)
 
@@ -46,6 +47,10 @@ Proof. eauto with typeclass_instances. Qed.
 Definition setoid_trans [ sa : Setoid A ] : Transitive equiv.
 Proof. eauto with typeclass_instances. Qed.
 
+Existing Instance setoid_refl.
+Existing Instance setoid_sym.
+Existing Instance setoid_trans.
+
 (** Standard setoids. *)
 
 (* Program Instance eq_setoid : Setoid A := *)
@@ -142,11 +147,10 @@ Ltac obligations_tactic ::= morphism_tac.
 
 Program Instance iff_impl_id_morphism : ? Morphism (iff ++> impl) id.
 
-Program Instance eq_arrow_id_morphism : ? Morphism (eq +++> arrow) id.
+(* Program Instance eq_arrow_id_morphism : ? Morphism (eq +++> arrow) id. *)
 
 (* Definition compose_respect (A B C : Type) (R : relation (A -> B)) (R' : relation (B -> C)) *)
 (*   (x y : A -> C) : Prop := forall (f : A -> B) (g : B -> C), R f f -> R' g g. *)
-    
 
 (* Program Instance (A B C : Type) (R : relation (A -> B)) (R' : relation (B -> C)) *)
 (*   [ mg : ? Morphism R' g ] [ mf : ? Morphism R f ] =>  *)