| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
|
|
