aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2020-10-15 17:39:39 +0200
committerEmilio Jesus Gallego Arias2020-11-18 14:09:04 +0100
commite0380f347d2ebf61b81760a365eea8c84ad3ada4 (patch)
tree40aac9bca9dd3cf59d94069b40a5e960e2d52bff /doc/plugin_tutorial
parent162c19cbb1863e11a81450a188a6d7f9f79e8b73 (diff)
[attributes] Allow boolean, single-value attributes.
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.
Diffstat (limited to 'doc/plugin_tutorial')
0 files changed, 0 insertions, 0 deletions