From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta

---
 test-suite/success/evars.v | 71 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 71 insertions(+)

(limited to 'test-suite/success/evars.v')

diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index 6423ad14..2f1ec757 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -238,3 +238,74 @@ eapply f_equal with (* should fail because ill-typed *)
         end) in H
 || injection H.
 Abort.
+
+(* A legitimate simple eapply that was failing in coq <= 8.3.
+   Cf. in Unification.w_merge the addition of an extra pose_all_metas_as_evars
+   on 30/9/2010
+*)
+
+Lemma simple_eapply_was_failing :
+ (forall f:nat->nat, exists g, f = g) -> True.
+Proof.
+ assert (modusponens : forall P Q, P -> (P->Q) -> Q) by auto.
+ intros.
+ eapply modusponens.
+ simple eapply H.
+ (* error message with V8.3 :
+    Impossible to unify "?18" with "fun g : nat -> nat => ?6 = g". *)
+Abort.
+
+(* Regression test *)
+
+Definition fo : option nat -> nat := option_rec _ (fun a => 0) 0.
+
+(* This example revealed an incorrect evar restriction at some time
+   around October 2011 *)
+
+Goal forall (A:Type) (a:A) (P:forall A, A -> Prop), (P A a) /\ (P A a).
+intros.
+refine ((fun H => conj (proj1 H) (proj2 H)) _).
+Abort.
+
+(* The argument of e below failed to be inferred from r14219 (Oct 2011) to *)
+(* r14753 after the restrictions made on detecting Miller's pattern in the *)
+(* presence of alias, only the second-order unification procedure was *)
+(* able to solve this problem but it was deactivated for 8.4 in r14219 *)
+
+Definition k0
+  (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat)
+  (j : forall a, exists n : nat, n = a) o :=
+ match o with (* note: match introduces an alias! *)
+ | Some a => e _ (j a)
+ | None => O
+ end.
+
+Definition k1
+  (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat)
+  (j : forall a, exists n : nat, n = a) a (b:=a) := e _ (j a).
+
+Definition k2
+  (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat)
+  (j : forall a, exists n : nat, n = a) a (b:=a) := e _ (j b).
+
+(* Other examples about aliases involved in pattern unification *)
+
+Definition k3
+  (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat)
+  (j : forall a, exists n : nat, let a' := a in n = a') a (b:=a) := e _ (j b).
+
+Definition k4
+  (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat)
+  (j : forall a, exists n : nat, let a' := S a in n = a') a (b:=a) := e _ (j b).
+
+Definition k5
+  (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat)
+  (j : forall a, let a' := S a in exists n : nat, n = a') a (b:=a) := e _ (j b).
+
+Definition k6
+  (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat)
+  (j : forall a, exists n : nat, let n' := S n in n' = a) a (b:=a) := e _ (j b).
+
+Definition k7
+  (e:forall P : nat -> Prop, (exists n : nat, let n' := n in P n') -> nat)
+  (j : forall a, exists n : nat, n = a) a (b:=a) := e _ (j b).
-- 
cgit v1.2.3