diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-04-13 12:13:04 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-04-13 12:31:02 +0200 |
| commit | 4e70791036a1ab189579e109b428f46f45698b59 (patch) | |
| tree | 4b3deb27bccb52fdafe19a75e065cbf1aec2d299 /test-suite/success/boundvars.v | |
| parent | 97f1d0b6ddfce894941d34fc3b3e4c4df0efadd2 (diff) | |
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".
Diffstat (limited to 'test-suite/success/boundvars.v')
| -rw-r--r-- | test-suite/success/boundvars.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/test-suite/success/boundvars.v b/test-suite/success/boundvars.v new file mode 100644 index 000000000..7b6696af8 --- /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. + |