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.

1 files changed, 15 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/4467.v b/test-suite/bugs/closed/4467.v
new file mode 100644
index 000000000..6f8631d45
--- /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.