From dd56ef10395a2ced84612aa799690b034306806e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 26 Jul 2017 22:34:43 +0200
Subject: Fixing another regression with 8.4 wrt to βι-normalization of created
 hyps.

This one is a continuation of e2a8edaf59 which was βι-normalizing the
hypotheses created by a "match". We forgot to do it for "let" and
"if". This is what this commit is doing.
---
 test-suite/success/refine.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v
index 352abb2af5..4f6505f583 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.
-- 
cgit v1.2.3