3 files changed, 59 insertions, 0 deletions
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index deeab4cb6..fcce68b91 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -185,3 +185,19 @@ intro.
 eapply H.
 apply (forall B:Prop,B->B) || (instantiate (1:=True); exact I).
 Defined.
+
+(* Fine-tuning coercion insertion in presence of unfolding (bug #1883) *)
+
+Parameter name : Set.
+Definition atom := name.
+
+Inductive exp : Set :=
+  | var : atom -> exp.
+
+Coercion var : atom >-> exp.
+
+Axiom silly_axiom : forall v : exp, v = v -> False.
+
+Lemma silly_lemma : forall x : atom, False.
+intros x.
+apply silly_axiom with (v := x).  (* fails *)
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index 02f88b727..5aa78816b 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -36,3 +36,22 @@ Theorem Refl : forall P, P <-> P. tauto. Qed.
 Goal True.
 case Refl || ecase Refl.
 Abort.
+
+
+(* Submitted by B. Baydemir (bug #1882) *)
+
+Require Import List.
+
+Definition alist R := list (nat * R)%type.
+
+Section Properties.
+  Variables A : Type.
+  Variables a : A.
+  Variables E : alist A.
+
+  Lemma silly : E = E.
+  Proof.
+    clear. induction E.  (* this fails. *)
+  Abort.
+
+End Properties.
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index e117bf62f..082cbfbe1 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -186,3 +186,27 @@ refine
 Abort.
 
 End Additions_while.
+
+(* Two examples from G. Melquiond (bugs #1878 and #1884) *)
+
+Parameter F1 G1 : nat -> Prop.
+Goal forall x : nat, F1 x -> G1 x.
+refine (fun x H => proj2 (_ x H)).
+Abort.
+
+Goal forall x : nat, F1 x -> G1 x.
+refine (fun x H => proj2 (_ x H) _).
+Abort.
+
+(* Remark: the following example does not succeed any longer in 8.2 because,
+   the algorithm is more general and does exclude a solution that it should
+   exclude for typing reason. Handling of types and backtracking is still to
+   be done
+
+Section S.
+Variables A B : nat -> Prop.
+Goal forall x : nat, A x -> B x.
+refine (fun x H => proj2 (_ x H) _).
+Abort.
+End S.
+*)