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/opened | |
| parent | 92c6f1c84d454a0b33b4d0bcd7cc6bb891b8854c (diff) | |
| parent | c352873936db93c251c544383853474736f128d6 (diff) | |
Merge PR #9530: Remove `VtUnkown` classification
Reviewed-by: JasonGross
Reviewed-by: SkySkimmer
Diffstat (limited to 'test-suite/bugs/opened')
| -rw-r--r-- | test-suite/bugs/opened/bug_3890.v | 22 |
1 files changed, 0 insertions, 22 deletions
diff --git a/test-suite/bugs/opened/bug_3890.v b/test-suite/bugs/opened/bug_3890.v deleted file mode 100644 index 9d83743b2a..0000000000 --- a/test-suite/bugs/opened/bug_3890.v +++ /dev/null @@ -1,22 +0,0 @@ -Set Nested Proofs Allowed. - -Class Foo. -Class Bar := b : Type. - -Set Refine Instance Mode. -Instance foo : Foo := _. -Unset Refine Instance Mode. -(* 1 subgoals, subgoal 1 (ID 4) - - ============================ - Foo *) - -Instance bar : Bar. -exact Type. -Defined. -(* bar is defined *) - -About foo. -(* foo not a defined object. *) - -Fail Defined. |