From c352873936db93c251c544383853474736f128d6 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 25 Jan 2019 00:48:36 +0100
Subject: Remove VtUnknown classification

This clean-up removes the dependency of the current proof mode (and hence
the parsing state) on unification.

The current proof mode can now be known simply by parsing and elaborating
attributes. We give access to attributes from the classifier for this purpose.

We remove the infamous `VtUnknown` code path in the STM which is known to
be buggy.

Fixes #3632 #3890 #4638.
---
 test-suite/bugs/opened/bug_3890.v | 22 ----------------------
 1 file changed, 22 deletions(-)
 delete mode 100644 test-suite/bugs/opened/bug_3890.v

(limited to 'test-suite/bugs/opened')

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.
-- 
cgit v1.2.3