diff options
| author | Pierre-Marie Pédrot | 2019-07-12 16:42:06 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-07-18 17:02:05 +0200 |
| commit | b8f77d00c586fd17c8447ab6fc74acf97b5597c4 (patch) | |
| tree | da714822d9dec8f224942ee89e318c3f098d7337 /vernac | |
| parent | 8dbdc3aab8e1f905522ec317fcdad5df82c93087 (diff) | |
Polymorphism attribute on section sets the option locally.
This is deemed to be more natural as most of the uses will follow this
structure.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacentries.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index e98a15eecc..46ddf214ab 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -965,7 +965,8 @@ let vernac_include l = let vernac_begin_section ~poly ({v=id} as lid) = Dumpglob.dump_definition lid true "sec"; - Lib.open_section ~poly id + Lib.open_section ~poly id; + set_bool_option_value_gen ~locality:OptLocal ["Universe"; "Polymorphism"] poly let vernac_end_section {CAst.loc} = Dumpglob.dump_reference ?loc |