Imported Upstream version 8.5~beta1+dfsg

1 files changed, 12 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/2930.v b/test-suite/bugs/closed/2930.v
new file mode 100644
index 00000000..0994b6fb
--- /dev/null
+++ b/test-suite/bugs/closed/2930.v
@@ -0,0 +1,12 @@
+(* Checking that let-in's hiding evars are expanded when enforcing
+   "occur-check" *)
+
+Require Import List.
+
+Definition foo x y :=
+let xy := (x, y) in
+let bar xys  :=
+      match xys with
+      | nil => xy :: nil
+      | xy' :: xys' => xy' :: xys'
+      end in bar (nil : list (nat * nat)).