diff options
| author | Pierre-Marie Pédrot | 2019-06-27 15:09:40 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-07-18 17:00:54 +0200 |
| commit | c13a3b61c9b1a714c50bcf0ec371a4effe1ff627 (patch) | |
| tree | f79625d7022c38673989e02247d2558754af0d32 /vernac | |
| parent | f8f77bb08968d6df7a4de3a8308b3069bcf15f0d (diff) | |
Attach the universe polymorphic status to sections.
The previous implementation allowed to dynamically decide whether a section
would be monomorphic or polymorphic at the first definition of a variable
or a constraint. Instead of relying on this delayed decision, we set the
universe polymorphic property directly at the time of the section definition.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacentries.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 68b7462bde..e98a15eecc 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -963,9 +963,9 @@ let vernac_include l = (* Sections *) -let vernac_begin_section ({v=id} as lid) = +let vernac_begin_section ~poly ({v=id} as lid) = Dumpglob.dump_definition lid true "sec"; - Lib.open_section id + Lib.open_section ~poly id let vernac_end_section {CAst.loc} = Dumpglob.dump_reference ?loc @@ -2396,8 +2396,7 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with (* Gallina extensions *) | VernacBeginSection lid -> VtNoProof(fun () -> - unsupported_attributes atts; - vernac_begin_section lid) + vernac_begin_section ~poly:(only_polymorphism atts) lid) | VernacEndSegment lid -> VtNoProof(fun () -> unsupported_attributes atts; |