diff options
| author | Maxime Dénès | 2019-01-14 11:42:48 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-01-14 11:42:48 +0100 |
| commit | c5d4472e3df352188123a90ef53b7383d9e1ba55 (patch) | |
| tree | e082d430bfac0ef5b4bd3bc1e4744c9899fda23f /test-suite | |
| parent | ac8c25a9fac51745f0b53162fba48ef5b86d227d (diff) | |
| parent | cf5d2818f34b606beafab58524396b97db51ac24 (diff) | |
Merge PR #9307: Handle local definitions in implicit arguments of Instance
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/bug_9300.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_9300.v b/test-suite/bugs/closed/bug_9300.v new file mode 100644 index 0000000000..a80f3233a3 --- /dev/null +++ b/test-suite/bugs/closed/bug_9300.v @@ -0,0 +1,6 @@ +Existing Class True. + +Instance foo {n : nat} (x := I) : forall {b : bool} (s : nat * nat), True. auto. Defined. + +Fail Check foo (n := 3) true (s := (4 , 5)). +Check foo (n := 3) (b := true) (4 , 5). |