From 4e70791036a1ab189579e109b428f46f45698b59 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 13 Apr 2017 12:13:04 +0200
Subject: Adding a fold_glob_constr_with_binders combinator.

Binding generalizable_vars_of_glob_constr, occur_glob_constr,
free_glob_vars, and bound_glob_vars on it.

Most of the functions of which it factorizes the code were bugged with
respect to bindings in the return clause of "match" and in either the
types or the bodies of "fix/cofix".
---
 test-suite/.csdp.cache         | Bin 89077 -> 89077 bytes
 test-suite/success/boundvars.v |   5 +++++
 2 files changed, 5 insertions(+)
 create mode 100644 test-suite/success/boundvars.v

(limited to 'test-suite')

diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache
index ba85286dd3..b99d80e95f 100644
Binary files a/test-suite/.csdp.cache and b/test-suite/.csdp.cache differ
diff --git a/test-suite/success/boundvars.v b/test-suite/success/boundvars.v
new file mode 100644
index 0000000000..7b6696af8e
--- /dev/null
+++ b/test-suite/success/boundvars.v
@@ -0,0 +1,5 @@
+(* An example showing a bug in the detection of free variables *)
+(* "x" is not free in the common type of "x" and "y" *)
+
+Check forall (x z:unit) (x y : match z as x return x=x with tt => eq_refl end = eq_refl), x=x.
+
-- 
cgit v1.2.3


From b4936da085b19ad508346d8e07ce1e922ef79c2d Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 13 Apr 2017 15:05:16 +0200
Subject: Using fold_glob_constr_with_binders to code bound_glob_vars.

To use the generic combinator, we introduce a side effect. I believe
that we have more to gain from a short code than from being purely
functional.

This also fixes the expected semantics since the variables binding the
return type in "match" were not taking into account.
---
 test-suite/.csdp.cache         | Bin 89077 -> 89077 bytes
 test-suite/success/boundvars.v |   9 +++++++++
 2 files changed, 9 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache
index b99d80e95f..ba85286dd3 100644
Binary files a/test-suite/.csdp.cache and b/test-suite/.csdp.cache differ
diff --git a/test-suite/success/boundvars.v b/test-suite/success/boundvars.v
index 7b6696af8e..fafe272925 100644
--- a/test-suite/success/boundvars.v
+++ b/test-suite/success/boundvars.v
@@ -3,3 +3,12 @@
 
 Check forall (x z:unit) (x y : match z as x return x=x with tt => eq_refl end = eq_refl), x=x.
 
+(* An example showing a bug in the detection of bound variables *)
+
+Goal forall x, match x return x = x with 0 => eq_refl | _ => eq_refl end = eq_refl.
+intro.
+match goal with
+|- (match x as y in nat return y = y with O => _ | S n => _ end) = _ => assert (forall y, y = 0) end.
+intro.
+Check x0. (* Check that "y" has been bound to "x0" while matching "match x as x0 return x0=x0 with ... end" *)
+Abort.
-- 
cgit v1.2.3