Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg

1 files changed, 15 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/2017.v b/test-suite/bugs/closed/shouldsucceed/2017.v
new file mode 100644
index 00000000..948cea3e
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2017.v
@@ -0,0 +1,15 @@
+(* Some check of Miller's pattern inference - used to fail in 8.2 due
+   first to the presence of aliases, secondly due to the absence of
+   restriction of the potential interesting variables to the subset of
+   variables effectively occurring in the term to instantiate *)
+
+Set Implicit Arguments.
+
+Variable choose : forall(P : bool -> Prop)(H : exists x, P x), bool.
+
+Variable H : exists x : bool, True.
+ 
+Definition coef :=
+match Some true	with
+  Some _ => @choose _ H |_ => true 
+end .