diff options
| author | Maxime Dénès | 2019-01-25 00:48:36 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-05-20 10:50:05 +0200 |
| commit | c352873936db93c251c544383853474736f128d6 (patch) | |
| tree | 543c33e11bbd4d980dfef55cc2ab5d65caf86a74 /test-suite/bugs/opened | |
| parent | a6757b089e1d268517bcba48a9fe33aa47526de2 (diff) | |
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.
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. |