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 /plugins | |
| 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 'plugins')
| -rw-r--r-- | plugins/ltac/g_rewrite.mlg | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg index 469551809c..12b12bc7b0 100644 --- a/plugins/ltac/g_rewrite.mlg +++ b/plugins/ltac/g_rewrite.mlg @@ -278,7 +278,7 @@ VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF } | #[ atts = rewrite_attributes; ] ![ proof ] [ "Add" "Morphism" constr(m) ":" ident(n) ] (* This command may or may not open a goal *) - => { VtUnknown, VtNow } + => { (if Lib.is_modtype() then VtSideff([n]) else VtStartProof(GuaranteesOpacity, [n])), VtLater } -> { add_morphism_infer atts m n } |