From 9f8ae1aa2678944888d80ce0867bfb2bba0c8c71 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 12 Jan 2016 22:12:40 +0100
Subject: Fixing #4467 (missing shadowing of variables in cases pattern).

This fixes a TODO in map_constr_expr_with_binders, a bug in
is_constructor, as well as a bug and TODOS in ids_of_cases_indtype.
---
 test-suite/bugs/closed/4467.v | 15 +++++++++++++++
 1 file changed, 15 insertions(+)
 create mode 100644 test-suite/bugs/closed/4467.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/4467.v b/test-suite/bugs/closed/4467.v
new file mode 100644
index 0000000000..6f8631d458
--- /dev/null
+++ b/test-suite/bugs/closed/4467.v
@@ -0,0 +1,15 @@
+(* Fixing missing test for variable shadowing *)
+
+Definition test (x y:bool*bool) :=
+  match x with
+  | (e as e1, (true) as e2)
+  | ((true) as e1, e as e2) =>
+    let '(e, b) := y in
+    e
+  | _ => true
+  end.
+
+Goal test (true,false) (true,true) = true.
+(* used to evaluate to "false = true" in 8.4 *)
+reflexivity.
+Qed.
-- 
cgit v1.2.3