diff options
| author | Gaëtan Gilbert | 2019-05-20 13:03:45 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-05-20 13:03:45 +0200 |
| commit | a5304d0a613141dd5008410034ae4b104f0fc06a (patch) | |
| tree | 6511a25b2e68602e4dc2bd96b2d1968c5cfd8a30 /test-suite/bugs/closed/bug_4580.v | |
| parent | 92c6f1c84d454a0b33b4d0bcd7cc6bb891b8854c (diff) | |
| parent | c352873936db93c251c544383853474736f128d6 (diff) | |
Merge PR #9530: Remove `VtUnkown` classification
Reviewed-by: JasonGross
Reviewed-by: SkySkimmer
Diffstat (limited to 'test-suite/bugs/closed/bug_4580.v')
| -rw-r--r-- | test-suite/bugs/closed/bug_4580.v | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/test-suite/bugs/closed/bug_4580.v b/test-suite/bugs/closed/bug_4580.v index a8a446cc9b..3f40569d61 100644 --- a/test-suite/bugs/closed/bug_4580.v +++ b/test-suite/bugs/closed/bug_4580.v @@ -2,6 +2,5 @@ Require Import Program. Class Foo (A : Type) := foo : A. -Unset Refine Instance Mode. Program Instance f1 : Foo nat := S _. Next Obligation. exact 0. Defined. |