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/success/boundvars.v | 9 +++++++++ 1 file changed, 9 insertions(+) (limited to 'test-suite/success') diff --git a/test-suite/success/boundvars.v b/test-suite/success/boundvars.v index 7b6696af8..fafe27292 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