diff options
| author | Gaëtan Gilbert | 2019-09-27 17:26:26 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-02 14:38:48 +0200 |
| commit | 994edaf989c0232b5c7de70a2f8ccb46c557da95 (patch) | |
| tree | 46f5633c8e3e351a232836f951b8946f71dcf256 /vernac | |
| parent | 77fd11a9f012a2878e13451e9d8a9f500c6392eb (diff) | |
Loosen restrictions on mixing universe mono/polymorphism in sections
We disallow adding univ constraints wich refer to polymorphic
universes, and monomorphic constants and inductives when polymorphic
universes or constraints are present.
Every other combination is already correctly discharged by the kernel.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacentries.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 43b58d6d4b..c3be57eec8 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -980,7 +980,9 @@ 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 id; + (* If there was no polymorphism attribute this just sets the option + to its current value ie noop. *) set_bool_option_value_gen ~locality:OptLocal ["Universe"; "Polymorphism"] poly let vernac_end_section {CAst.loc} = |