diff options
Diffstat (limited to 'test-suite/bugs/closed')
| -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). |