Minor fixes. Use expanded type in class_tactics for Morphism search, to

alleviate some problems with delta. Better precedence in lambda
notation. Temporarily deactivate notations for relation conjunction,
equivalence and so on, while we search for a better syntax and maybe a
generalization (fixes bug #1820). Better destruct_call in
Program.Tactics.


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

2 files changed, 8 insertions, 12 deletions

diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 3a029371b4..d10cb97242 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -20,8 +20,6 @@ Require Import Coq.Program.Tactics.
 Require Import Coq.Relations.Relation_Definitions.
 Require Export Coq.Classes.RelationClasses.
 
-Open Local Scope relation_scope.
-
 Set Implicit Arguments.
 Unset Strict Implicit.
 
@@ -447,7 +445,7 @@ Proof.
 Qed.
 
 Lemma inverse_respectful : forall (A : Type) (R : relation A) (B : Type) (R' : relation B),
-  inverse (R ==> R') <R> (inverse R ==> inverse R').
+  relation_equivalence (inverse (R ==> R')) (inverse R ==> inverse R').
 Proof.
   intros.
   unfold flip, respectful.
@@ -593,5 +591,5 @@ Program Instance {A : Type} => all_inverse_impl_morphism :
   Qed.
 
 Lemma inverse_pointwise_relation A (R : relation A) : 
-  pointwise_relation (inverse R) <R> inverse (pointwise_relation (A:=A) R).
+  relation_equivalence (pointwise_relation (inverse R)) (inverse (pointwise_relation (A:=A) R)).
 Proof. reflexivity. Qed.
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 6ef2f756d3..f5d3cc1c45 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -217,26 +217,24 @@ Program Instance [ sa : Equivalence a R, sb : Equivalence b R' ] => equiv_setoid
 Definition relation_equivalence {A : Type} : relation (relation A) :=
   fun (R R' : relation A) => forall x y, R x y <-> R' x y.
 
-Infix "<R>" := relation_equivalence (at level 95, no associativity) : relation_scope.
-
 Class subrelation {A:Type} (R R' : relation A) :=
   is_subrelation : forall x y, R x y -> R' x y.
 
 Implicit Arguments subrelation [[A]].
 
-Infix "-R>" := subrelation (at level 70) : relation_scope.
 
 Definition relation_conjunction {A} (R : relation A) (R' : relation A) : relation A :=
   fun x y => R x y /\ R' x y.
 
-Infix "/R\" := relation_conjunction (at level 80, right associativity) : relation_scope.
-
 Definition relation_disjunction {A} (R : relation A) (R' : relation A) : relation A :=
   fun x y => R x y \/ R' x y.
 
-Infix "\R/" := relation_disjunction (at level 85, right associativity) : relation_scope.
+(* Infix "<R>" := relation_equivalence (at level 95, no associativity) : relation_scope. *)
+(* Infix "-R>" := subrelation (at level 70) : relation_scope. *)
+(* Infix "/R\" := relation_conjunction (at level 80, right associativity) : relation_scope. *)
+(* Infix "\R/" := relation_disjunction (at level 85, right associativity) : relation_scope. *)
 
-Open Local Scope relation_scope.
+(* Open Local Scope relation_scope. *)
 
 (** Relation equivalence is an equivalence, and subrelation defines a partial order. *)
 
@@ -258,7 +256,7 @@ Program Instance subrelation_preorder :
    on the carrier. *)
 
 Class [ equ : Equivalence A eqA, PreOrder A R ] => PartialOrder :=
-  partial_order_equivalence : relation_equivalence eqA (R /R\ flip R).
+  partial_order_equivalence : relation_equivalence eqA (relation_conjunction R (flip R)).
 
 
 (** The equivalence proof is sufficient for proving that [R] must be a morphism