aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Classes
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-04-15 13:19:33 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-04-15 13:19:33 +0000
commit44e7deb7c82ec2ddddf551a227c67a76ccb3009a (patch)
tree1f5b7f0b0684059930e0567b2cecc194c1869aec /theories/Classes
parent07e03e167c7eda30ffc989530470b5c597beaedc (diff)
- Add "Global" modifier for instances inside sections with the usual
semantics. - Add an Equivalence instance for pointwise equality from an Equivalence on the codomain of a function type, used by default when comparing functions with the Setoid's ===/equiv. - Partially fix the auto hint database "add" function where the exact same lemma could be added twice (happens when doing load for example). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10797 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Classes')
-rw-r--r--theories/Classes/Equivalence.v12
1 files changed, 11 insertions, 1 deletions
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 4f794af3f..6270fb43b 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -178,4 +178,14 @@ Section Respecting.
symmetry. auto.
Qed.
-End Respecting. \ No newline at end of file
+End Respecting.
+
+(** The default equivalence on function spaces. *)
+
+Program Instance [ Equivalence A eqA ] =>
+ pointwise_equivalence : Equivalence (B -> A) (pointwise_relation eqA).
+
+ Next Obligation.
+ Proof.
+ transitivity (y x0) ; auto.
+ Qed.