Fixes in new Morphisms files.

- Use a notation for predicate instead of a
definition (better pretty-printing this way, and no delta
problem!).
- Correct inadvertent import of Coq.Program.Program which sets
implicit arguments for left,right and so on. Should fix the contribs
that used to compile. 
- Correct normalization_tac to do normalization of "inverse"
signatures. Add a missing instance, and name the existing ones.


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

1 files changed, 2 insertions, 2 deletions

diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v
index 274389496..5018fa01e 100644
--- a/theories/Classes/Morphisms_Relations.v
+++ b/theories/Classes/Morphisms_Relations.v
@@ -31,11 +31,11 @@ Instance relation_disjunction_morphism : Morphism (relation_equivalence (A:=A) =
 Require Import List.
 
 Lemma predicate_equivalence_pointwise (l : list Type) :
-  Morphism (@predicate_equivalence l ==> lift_pointwise l iff) id.
+  Morphism (@predicate_equivalence l ==> pointwise_lifting iff l) id.
 Proof. do 2 red. unfold predicate_equivalence. auto. Qed.
 
 Lemma predicate_implication_pointwise (l : list Type) :
-  Morphism (@predicate_implication l ==> lift_pointwise l impl) id.
+  Morphism (@predicate_implication l ==> pointwise_lifting impl l) id.
 Proof. do 2 red. unfold predicate_implication. auto. Qed.
 
 (** The instanciation at relation allows to rewrite applications of relations [R x y] to [R' x y] *)