diff options
author | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-21 13:57:03 +0000 |
---|---|---|
committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-21 13:57:03 +0000 |
commit | 880a83169c1d1df8726d301a9f8a9fc845cc7d1e (patch) | |
tree | 11f101429c8d8759b11a5b6589ec28e70585abcd /theories/Classes/Equivalence.v | |
parent | 6a8e2a2e13978b40f246563d7cfda0ec58370006 (diff) |
- Parameterize unification by two sets of transparent_state, one for open
term unification (for constant and variable delta unfolding) and one to
parameterize closed-term conversion. Most of the time conversion uses
full delta and unification does no delta. This fine-grain is used in
rewrite/setoid_rewrite, where only closed-term delta on global constants
is allowed.
- Interpret Hint Unfold as a directive for delta conversion in
auto/eauto when applying lemmas (i.e., for Resolve and Immediate hints).
- Remove ad-hoc support for this in typeclasses. Now setoid_rewrite
works correctly w.r.t. the old version regarding local definitions.
- Fix closed bugs which needed updating due to syntax modifications.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10824 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Classes/Equivalence.v')
-rw-r--r-- | theories/Classes/Equivalence.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index 5e34a4437..23af8a744 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -30,7 +30,7 @@ Open Local Scope signature_scope. Definition equiv [ Equivalence A R ] : relation A := R. -Typeclasses unfold @equiv. +Typeclasses unfold equiv. (** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *) @@ -44,7 +44,7 @@ Open Local Scope equiv_scope. Definition pequiv [ PER A R ] : relation A := R. -Typeclasses unfold @pequiv. +Typeclasses unfold pequiv. (** Overloaded notation for partial equivalence. *) |