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 /kernel/safe_typing.ml | |
| 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 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index db16bd1e79..4268f0a602 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 @@ -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 | _ :: _, [] -> |