diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-06 22:39:43 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-06 22:39:43 +0000 |
| commit | a1fe45ddbd37d3c447a23cde0ee21f105ef42ac0 (patch) | |
| tree | 648a977d3137ffa9c7cc97e8503c0a5d8620dbfa /theories/Classes/SetoidClass.v | |
| parent | 0cdfa2fb137989f75cdebfa3a64726bc0d56a8af (diff) | |
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
Diffstat (limited to 'theories/Classes/SetoidClass.v')
| -rw-r--r-- | theories/Classes/SetoidClass.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v index d22398166..c5a8f3d30 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. *) |