diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-17 18:54:40 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-03-17 18:54:40 +0000 |
| commit | 405a876ec06bc92168c2323b44a621734dff4901 (patch) | |
| tree | ee7452b2060013dde71af708a7a84fdbe69750e2 /theories/Classes/SetoidClass.v | |
| parent | a4e02939c27240159946dd037d85db4cf6af2ef1 (diff) | |
Add the possibility of specifying constants to unfold for typeclass
resolution. Add [relation] and Setoid's [equiv] as such objects.
Considerably simplify resolve_all_evars for typeclass resolution, adding
a further refinement (and hack): evars get classified as non-resolvable
(using the evar_extra dynamic field) if they are turned into a
goal. This makes it possible to perform nested typeclass resolution
without looping. We
take advantage of that in Classes/Morphisms where [subrelation_tac] is
added to the [Morphism] search procedure and calls the apply tactic which
itself triggers typeclass resolution. Having [subrelation_tac] as a tactic
instead of an instance, we can actually force that it is applied only
once in each search branch and avoid looping.
We could get rid of the hack when we have real goals-as-evars
functionality (hint hint).
Also fix some test-suite scripts which were still calling [refl]
instead of [reflexivity].
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10687 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Classes/SetoidClass.v')
| -rw-r--r-- | theories/Classes/SetoidClass.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v index b355c3c08..5cf33542c 100644 --- a/theories/Classes/SetoidClass.v +++ b/theories/Classes/SetoidClass.v @@ -8,7 +8,6 @@ (************************************************************************) (* Typeclass-based setoids, tactics and standard instances. - TODO: explain clrewrite, clsubstitute and so on. Author: Matthieu Sozeau Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud @@ -32,6 +31,8 @@ Class Setoid A := equiv : relation A ; setoid_equiv :> Equivalence A equiv. +Typeclasses unfold @equiv. + (* Too dangerous instance *) (* Program Instance [ eqa : Equivalence A eqA ] => *) (* equivalence_setoid : Setoid A := *) |