| Age | Commit message (Collapse) | Author |
|---|
|
The syntax is the one of boolean attributes, that is to say
`#[typing($flag={yes,no}]` where `$flag` is one of `guarded`,
`universes`, `positive`.
We had to instrument the pretyper in a few places, it is interesting
that it is doing so many checks.
|
|
We introduce a warning so boolean attributes are expected to be of the
form `attr={yes,no}` or just `attr` (for `yes`).
We update the documentation, test-suite, and changelog.
|
|
Following discussion in https://github.com/coq/coq/pull/12586 , we
extend the syntax `val=string` to support also arbitrary values.
In particular we support boolean ones, or arbitrary key-pair lists.
This complements the current form `val="string"`, and makes more sense
in general.
Current syntax for the boolean version is `attr=yes` or `attr=no`, but
we could be more liberal if desired.
The general new guideline is that `foo(vals)` is reserved for
the case where `vals` is a list, whereas `foo=val` is for attributes
that allow a unique assignment.
This commit only introduces the support, next commits will migrate
some attributes to this new syntax and deprecate the old versions.
|
|
|
|
Reviewed-by: jfehrle
|
|
Add headers to a few files which were missing them.
|
|
|
|
They were already deprecated in two major releases.
|
|
|
|
|
|
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.
|
|
This is a pre-requisite to use automated formatting tools such as
`ocamlformat`, also, there were quite a few places where the comments
had basically no effect, thus it was confusing for the developer.
p.s: Reading some comments was a lot of fun :)
|
|
|
|
|
|
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.
|
|
|
