3 files changed, 17 insertions, 1 deletions
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.