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 | |
| 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')
| -rw-r--r-- | test-suite/.csdp.cache | bin | 89077 -> 89077 bytes | |||
| -rw-r--r-- | test-suite/success/boundvars.v | 5 |
2 files changed, 5 insertions, 0 deletions
diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache Binary files differindex ba85286dd..b99d80e95 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 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. + |