diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-04-13 15:05:16 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-04-13 15:16:51 +0200 |
| commit | b4936da085b19ad508346d8e07ce1e922ef79c2d (patch) | |
| tree | 8a51b2bead7486af7f0a59efc6c4882f2d5cc087 /test-suite/success/boundvars.v | |
| parent | 4e70791036a1ab189579e109b428f46f45698b59 (diff) | |
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.
Diffstat (limited to 'test-suite/success/boundvars.v')
| -rw-r--r-- | test-suite/success/boundvars.v | 9 |
1 files changed, 9 insertions, 0 deletions
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. |