diff options
| author | Hugo Herbelin | 2017-04-13 15:05:16 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-04-13 15:16:51 +0200 |
| commit | b4936da085b19ad508346d8e07ce1e922ef79c2d (patch) | |
| tree | 8a51b2bead7486af7f0a59efc6c4882f2d5cc087 /test-suite | |
| 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')
| -rw-r--r-- | test-suite/.csdp.cache | bin | 89077 -> 89077 bytes | |||
| -rw-r--r-- | test-suite/success/boundvars.v | 9 |
2 files changed, 9 insertions, 0 deletions
diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache Binary files differindex b99d80e95f..ba85286dd3 100644 --- a/test-suite/.csdp.cache +++ b/test-suite/.csdp.cache 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. |