diff options
| author | Hugo Herbelin | 2019-05-21 14:18:51 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-05-21 20:48:42 +0200 |
| commit | c7f1470c69bf5e8e823550fe94c28fc5fa33e712 (patch) | |
| tree | 8cdbde50b7ee3f1e80d6cecaf6d005dfe78877ac | |
| parent | d14be61b4468573d7aa184fe6c8a0a7c8d5a0044 (diff) | |
Adding test for old bug fixed in 8.5 (wrong implicit arguments in fixpoint).
| -rw-r--r-- | test-suite/bugs/closed/bug_3810.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/bug_3810.v b/test-suite/bugs/closed/bug_3810.v new file mode 100644 index 0000000000..0b2bef8a9b --- /dev/null +++ b/test-suite/bugs/closed/bug_3810.v @@ -0,0 +1,6 @@ +Class Foo. + +Fixpoint test (H : Foo) (n : nat) {A : Type} {struct n} : A. +Admitted. + +Check fun (x:Foo) => test x 0. |