diff options
author | 2017-05-05 18:11:58 +0200 | |
---|---|---|
committer | 2017-05-05 18:11:58 +0200 | |
commit | cd76a274c7d6fb71e109b6f3c87dd3a661f72e6c (patch) | |
tree | 78b77f070e9afbc3257487234c973eb895cc21f4 /test-suite/success | |
parent | a76a71eda10b054b04de4ff56f0637a32077edd4 (diff) | |
parent | b4936da085b19ad508346d8e07ce1e922ef79c2d (diff) |
Merge PR#558: Adding a fold_glob_constr_with_binders combinator
Diffstat (limited to 'test-suite/success')
-rw-r--r-- | test-suite/success/boundvars.v | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/test-suite/success/boundvars.v b/test-suite/success/boundvars.v new file mode 100644 index 000000000..fafe27292 --- /dev/null +++ b/test-suite/success/boundvars.v @@ -0,0 +1,14 @@ +(* 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. + +(* 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. |