From b31a26f32f2600ba88653086a871dc1fafce4d4d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 25 Oct 2011 13:31:49 +0000
Subject: New strategy to infer return predicate of match construct when
 external type has evars. We now create a new ad hoc evar instead of having
 evars as arguments of evars and use filters to resolved them as was done
 since about r10124. In particular, this completes the resolution of bug 2615.

Evar filters for occurrences might be obsolete as a consequence of
this commit.

Also, abstract_tycon, evar_define, second_order_matching which all
implement some form of second_order_matching should eventually be
merged (abstract_tycon looks for subterms up to delta while
second_order_matching currently looks for syntactic equal subterms,
evar_define doesn't consider the possible dependencies in
non-variables-nor-constructors subterms but has a better handling of
aliases, ...).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14592 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/bugs/closed/shouldsucceed/2615.v | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/shouldsucceed/2615.v b/test-suite/bugs/closed/shouldsucceed/2615.v
index 005491637d..54e1a07cc8 100644
--- a/test-suite/bugs/closed/shouldsucceed/2615.v
+++ b/test-suite/bugs/closed/shouldsucceed/2615.v
@@ -6,3 +6,9 @@ Inductive foo : forall A, A -> Prop :=
 Lemma bar A B f : foo (A -> B) f -> forall x : A, foo B (f x).
 Fail induction 1.
 
+(* Whether these examples should succeed with a non-dependent return predicate 
+   or fail because there is well-typed return predicate dependent in f 
+   is questionable. As of 25 oct 2011, they succeed *)
+refine (fun p => match p with _ => _ end).
+Undo.
+refine (fun p => match p with foo_intro _ _ => _ end).
-- 
cgit v1.2.3