aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Classes/Equivalence.v
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-06-27 15:52:05 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-06-27 15:52:05 +0000
commit64ac193d372ef8428e85010a862ece55ac011192 (patch)
treed64af209e0a97f652918f500c3dd6a0ba1431bb7 /theories/Classes/Equivalence.v
parent7b74581cd633d28c83589dff1adf060fcfe87e8a (diff)
Enhanced discrimination nets implementation, which can now work with
goals containing existentials and use transparency information on constants (optionally). Only used by the typeclasses eauto engine for now, but could be used for other hint bases easily (just switch a boolean). Had to add a new "creation" hint to be able to set said boolean upon creation of the typeclass_instances hint db. Improve the proof-search algorithm for Morphism, up to 10 seconds gained in e.g. Field_theory, Ring_polynom. Added a morphism declaration for [compose]. One needs to declare more constants as being unfoldable using the [Typeclasses unfold] command so that discrimination is done correctly, but that amounts to only 6 declarations in the standard library. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11184 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Classes/Equivalence.v')
-rw-r--r--theories/Classes/Equivalence.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index 42961baea..d77704c12 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -134,8 +134,8 @@ End Respecting.
(** The default equivalence on function spaces, with higher-priority than [eq]. *)
-Program Instance pointwise_equivalence [ Equivalence A eqA ] :
- Equivalence (B -> A) (pointwise_relation eqA) | 9.
+Program Instance pointwise_equivalence [ Equivalence B eqB ] :
+ Equivalence (A -> B) (pointwise_relation eqB) | 9.
Next Obligation.
Proof.