diff options
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 11 |
1 files changed, 4 insertions, 7 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index db16bd1e79..1069d9a62c 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -334,8 +334,6 @@ type constraints_addition = let push_context_set poly cst senv = if Univ.ContextSet.is_empty cst then senv - else if Section.is_polymorphic senv.sections then - CErrors.user_err (Pp.str "Cannot add global universe constraints inside a polymorphic section.") else let sections = if Section.is_empty senv.sections then senv.sections @@ -735,7 +733,7 @@ let constant_entry_of_side_effect eff = if Declareops.is_opaque cb then OpaqueEff { opaque_entry_body = Future.from_val ((p, Univ.ContextSet.empty), ()); - opaque_entry_secctx = cb.const_hyps; + opaque_entry_secctx = Context.Named.to_vars cb.const_hyps; opaque_entry_feedback = None; opaque_entry_type = cb.const_type; opaque_entry_universes = univs; @@ -743,7 +741,7 @@ let constant_entry_of_side_effect eff = else DefinitionEff { const_entry_body = p; - const_entry_secctx = Some cb.const_hyps; + const_entry_secctx = Some (Context.Named.to_vars cb.const_hyps); const_entry_feedback = None; const_entry_type = Some cb.const_type; const_entry_universes = univs; @@ -947,13 +945,13 @@ let add_module l me inl senv = (** {6 Interactive sections *) -let open_section ~poly senv = +let open_section senv = let custom = { rev_env = senv.env; rev_univ = senv.univ; rev_objlabels = senv.objlabels; } in - let sections = Section.open_section ~poly ~custom senv.sections in + let sections = Section.open_section ~custom senv.sections in { senv with sections } let close_section senv = @@ -962,7 +960,6 @@ let close_section senv = let env0 = senv.env in (* First phase: revert the declarations added in the section *) let sections, entries, cstrs, revert = Section.close_section sections0 in - let () = assert (not (Section.is_polymorphic sections0) || Univ.ContextSet.is_empty cstrs) in let rec pop_revstruct accu entries revstruct = match entries, revstruct with | [], revstruct -> accu, revstruct | _ :: _, [] -> |