Enhancements to coqdoc, better globalization of sections and modules.

Minor fix in Morphisms which prevented working with higher-order
morphisms and PER relations.


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

2 files changed, 3 insertions, 3 deletions

diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index cd38f318cf..6885d0b294 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -336,7 +336,7 @@ Proof. firstorder. Qed.
 
 (** [R] is Reflexive, hence we can build the needed proof. *)
 
-Lemma Reflexive_partial_app_morphism [ Morphism (A -> B) (R ==> R') m, Reflexive A R ] (x : A) :
+Lemma Reflexive_partial_app_morphism [ Morphism (A -> B) (R ==> R') m, MorphismProxy A R x ] :
    Morphism R' (m x).
 Proof. simpl_relation. Qed.
 
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index d22398166f..c5a8f3d308 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -131,7 +131,7 @@ Implicit Arguments setoid_morphism [[!sa]].
 Existing Instance setoid_morphism.
 
 Program Definition setoid_partial_app_morphism [ sa : Setoid A ] (x : A) : Morphism (equiv ++> iff) (equiv x) :=
-  Reflexive_partial_app_morphism x.
+  Reflexive_partial_app_morphism.
 
 Existing Instance setoid_partial_app_morphism.
 
@@ -148,7 +148,7 @@ Ltac obligations_tactic ::= morphism_tac.
    using [iff_impl_id_morphism] if the proof is in [Prop] and
    [eq_arrow_id_morphism] if it is in Type. *)
 
-Program Instance iff_impl_id_morphism : Morphism (iff ++> impl) id.
+Program Instance iff_impl_id_morphism : Morphism (iff ++> impl) Basics.id.
 
 (* Program Instance eq_arrow_id_morphism : ? Morphism (eq +++> arrow) id. *)