5 files changed, 50 insertions, 2 deletions
diff --git a/test-suite/bugs/closed/5245.v b/test-suite/bugs/closed/5245.v
index 77bf169e18..e5bca5b5e4 100644
--- a/test-suite/bugs/closed/5245.v
+++ b/test-suite/bugs/closed/5245.v
@@ -15,4 +15,4 @@ Undo.
 progress hnf; intros; exact eq_refl.
 Undo.
 unfold foo_rel. intros x. exact eq_refl.
-Qed.
-\ No newline at end of file
+Qed.
diff --git a/test-suite/bugs/closed/6070.v b/test-suite/bugs/closed/6070.v
new file mode 100644
index 0000000000..49b16f6254
--- /dev/null
+++ b/test-suite/bugs/closed/6070.v
@@ -0,0 +1,32 @@
+(* A slight shortening of bug 6078 *)
+
+(* This bug exposed a different behavior of unshelve_unifiable
+   depending on which projection is found in the unification
+   heuristics *)
+
+Axiom flat_type : Type.
+Axiom interp_flat_type : flat_type -> Type.
+Inductive type := Arrow (_ _ : flat_type).
+Definition interp_type (t : type)
+  := interp_flat_type (match t with Arrow s d => s end)
+     -> interp_flat_type (match t with Arrow s d => d end).
+Axiom Expr : type -> Type.
+Axiom Interp : forall {t : type}, Expr t -> interp_type t.
+Axiom Wf : forall {t}, Expr t -> Prop.
+Axiom a : forall f, interp_flat_type f.
+
+Definition packaged_expr_functionP A :=
+  (fun F : Expr A -> Expr A
+   => forall e' v, Interp (F e') v = a (let (_,f) := A in f)).
+Goal forall (f f0 : flat_type)
+            (e : forall _ : Expr (@Arrow f f0),
+                Expr (@Arrow f f0)),
+    @packaged_expr_functionP (@Arrow f f0) e.
+  intros.
+  refine (fun (e0 : Expr (Arrow f f0))
+   => (fun zHwf':True =>
+   (fun v : interp_flat_type f =>
+      ?[G] : ?[U] = ?[V] :> interp_flat_type ?[v])) ?[H]);
+   [ | ].
+   (* Was: Error: Tactic failure: Incorrect number of goals (expected 3 tactics). *)
+Abort.
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index 0219c3bfdf..6fbe61a9be 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -430,3 +430,9 @@ eexists ?[x].
 destruct (S _).
 change (0 = ?x).
 Abort.
+
+Goal (forall P, P 0 -> True/\True) -> True.
+intro H.
+destruct (H (fun x => True)).
+match goal with |- True => idtac end.
+Abort.
diff --git a/test-suite/success/guard.v b/test-suite/success/guard.v
index 83d47dc683..3a1c6dabeb 100644
--- a/test-suite/success/guard.v
+++ b/test-suite/success/guard.v
@@ -25,4 +25,4 @@ match f with
     match e in (_ = B) return (B -> foo A) -> nat with
     | eq_refl => fun (g' : nat -> foo A) => bar A e (g' O)
     end g
-end e.
-\ No newline at end of file
+end e.
diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v
index b8a8ff7561..22fb4d7576 100644
--- a/test-suite/success/refine.v
+++ b/test-suite/success/refine.v
@@ -122,3 +122,13 @@ Abort.
 
 Goal (forall A : Prop, A -> ~~A).
 Proof. refine(fun A a f => _).
+
+(* Checking beta-iota normalization of hypotheses in created evars *)
+
+Goal {x|x=0} -> True.
+refine (fun y => let (x,a) := y in _).
+match goal with a:_=0 |- _ => idtac end.
+
+Goal (forall P, {P 0}+{P 1}) -> True.
+refine (fun H => if H (fun x => x=x) then _ else _).
+match goal with _:0=0 |- _ => idtac end.