diff options
| author | Théo Zimmermann | 2020-03-18 19:45:21 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-03-19 18:05:04 +0100 |
| commit | 4b37834a2ed6a275daec1c98fac19795f96712ce (patch) | |
| tree | 35db898529e6843d0d0fb43b3b8779ac50224c29 /vernac/vernacexpr.ml | |
| parent | 82960d49d08372c345da972f16c3fbcc1c2073b1 (diff) | |
Interpret the Export modifier of Set and Unset as an attribute.
Unfortunately, we cannot go further and parse Export as a legacy
attribute because this syntax conflicts with the Export command.
Diffstat (limited to 'vernac/vernacexpr.ml')
| -rw-r--r-- | vernac/vernacexpr.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 67e1fb9495..b7c6d3c490 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -399,7 +399,7 @@ type nonrec vernac_expr = | VernacSetOpacity of (Conv_oracle.level * qualid or_by_notation list) | VernacSetStrategy of (Conv_oracle.level * qualid or_by_notation list) list - | VernacSetOption of export_flag * Goptions.option_name * option_setting + | VernacSetOption of bool (* Export modifier? *) * Goptions.option_name * option_setting | VernacAddOption of Goptions.option_name * option_ref_value list | VernacRemoveOption of Goptions.option_name * option_ref_value list | VernacMemOption of Goptions.option_name * option_ref_value list |