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 /vernac/vernacextend.mli | |
| 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 'vernac/vernacextend.mli')
| -rw-r--r-- | vernac/vernacextend.mli | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli index 4d89eaffd9..54e08d0e95 100644 --- a/vernac/vernacextend.mli +++ b/vernac/vernacextend.mli @@ -52,7 +52,6 @@ type vernac_type = | VtProofMode of string (* To be removed *) | VtMeta - | VtUnknown and vernac_start = opacity_guarantee * Names.Id.t list and vernac_sideff_type = Names.Id.t list and opacity_guarantee = |