aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-03-17 18:54:40 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-03-17 18:54:40 +0000
commit405a876ec06bc92168c2323b44a621734dff4901 (patch)
treeee7452b2060013dde71af708a7a84fdbe69750e2 /test-suite/bugs/closed
parenta4e02939c27240159946dd037d85db4cf6af2ef1 (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 'test-suite/bugs/closed')
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1704.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/1704.v b/test-suite/bugs/closed/shouldsucceed/1704.v
index 81b221690..4b02d5f93 100644
--- a/test-suite/bugs/closed/shouldsucceed/1704.v
+++ b/test-suite/bugs/closed/shouldsucceed/1704.v
@@ -12,6 +12,6 @@ Axiom r : False -> 0 == 1.
Goal 0 == 0.
Proof.
rewrite r.
-refl.
+reflexivity.
admit.
Qed.