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

1 files changed, 2 insertions, 4 deletions

diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 3a029371b..d10cb9724 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.