| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
Reviewed-by: jfehrle
|
|
Add headers to a few files which were missing them.
|
|
|
|
They were already deprecated in two major releases.
|
|
The standard use is to repeat the option keywords in lowercase, which
is basically useless.
En passant add doc entry for Dump Arith.
|
|
|
|
This means we can disable it to ignore unsupported attributes. For
instance this would be useful if we change some behaviour of `Cmd` and add an
attribute `att` to restore the old behaviour, then `#[att] Cmd` is
backwards compatible if the warning is disabled.
|
|
|
|
We also slightly change the semantics of the `compat` syntax modifier to
re-express it in terms of the `deprecated` attribute, and we deprecate
it in favor of the latter.
|
|
Attributes that enable/disable a feature can have an explicit value
(default is enable when the attribute is present).
Three-valued boolean attributes do not support this:
what would `#[local(false)]` mean?
|
|
|
|
We remove all calls to `Flags.is_program_mode` except one (to compute
the default value of the attribute). Everything else is passed
explicitely, and we remove the special logic in the interpretation loop
to set/unset the flag.
This is especially important since the value of the flag has an impact on
proof modes, so on the separation of parsing and execution phases.
|
|
|
|
|
|
|
|
We group the extension API and datatypes under `Vernacextend`.
This means that the base plugin dependency is now `coq.vernac` from
`coq.stm`.
This is quite important as for example the LSP server won't like to
link the STM in.
LTAC still depends on the STM by means of the ltac_profile part tho.
The next step could be to move the extension point below `Vernacexpr`.
|
|
|
|
|
|
|
|
Having [map] means we can structure attributes when combining them, eg
get an attribute for [type universe_data = { poly : bool option; template : bool
option }] from 2 [bool option] attributes.
Using the previous representation we would have had to provide the
inverse function [universe_data -> bool option * bool option] as well.
An alternate way to get (++) is
let (++) (x:'a t) (y:'b t) : ('a*'b) t =
x >>= fun xv ->
y >>= fun yv ->
return (xv,yv)
Not sure if that would be cleaner.
|
|
|
|
Commands need to request the attributes they use, with the API
encouraging them to error on unsupported attributes.
|
|
|
|
|
|
It was never set, because it makes no sense.
|
|
|
