diff options
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. + |