diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/evars.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v index dbace977e..ea1dd803f 100644 --- a/test-suite/success/evars.v +++ b/test-suite/success/evars.v @@ -56,3 +56,7 @@ Check :forall x : nat, (forall y n : nat, {q : nat | y = q * n}) -> forall n : nat, {q : nat | x = q * n}). + +(* Check instantiation of nested evars (bug #1089) *) + +Check (fun f:(forall (v:Set->Set), v (v nat) -> nat) => f _ (Some (Some O))). |