Test surgical use of beta-iota in the type of variables coming from

pattern-matching for refine.

1 files changed, 10 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/5219.v b/test-suite/bugs/closed/5219.v
new file mode 100644
index 0000000000..f7cec1a0cf
--- /dev/null
+++ b/test-suite/bugs/closed/5219.v
@@ -0,0 +1,10 @@
+(* Test surgical use of beta-iota in the type of variables coming from
+   pattern-matching for refine *)
+
+Goal forall x : sigT (fun x => x = 1), True.
+  intro x; refine match x with
+                  | existT _ x' e' => _
+                  end.
+  lazymatch goal with
+  | [ H : _ = _ |- _ ] => idtac
+  end.