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.ml | |
| 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.ml')
| -rw-r--r-- | vernac/vernacextend.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index ef06e59316..730f5fd6da 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -36,7 +36,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 = |