diff options
| author | Pierre-Marie Pédrot | 2021-01-11 16:41:19 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2021-01-11 16:52:10 +0100 |
| commit | 3c427cd52ad7e41b4a8cbb7e227b8f79730863b1 (patch) | |
| tree | 8b9de51ec0317b812c3bc873b72dd54310e03022 /vernac/declareUniv.ml | |
| parent | 76de13a9ce03f542bca74dabee28bf27d9d8ac4f (diff) | |
Do not declare a global universe object when the universe set is empty.
Diffstat (limited to 'vernac/declareUniv.ml')
| -rw-r--r-- | vernac/declareUniv.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/vernac/declareUniv.ml b/vernac/declareUniv.ml index 834ef0d29a..91ab17575d 100644 --- a/vernac/declareUniv.ml +++ b/vernac/declareUniv.ml @@ -74,6 +74,10 @@ let input_univ_names : universe_name_decl -> Libobject.obj = subst_function = (fun (subst, a) -> (* Actually the name is generated once and for all. *) a); classify_function = (fun a -> Substitute a) } +let input_univ_names (src, l) = + if CList.is_empty l then () + else Lib.add_anonymous_leaf (input_univ_names (src, l)) + let invent_name (named,cnt) u = let rec aux i = let na = Id.of_string ("u"^(string_of_int i)) in @@ -120,7 +124,7 @@ let declare_univ_binders gr pl = aux, (id,univ) :: univs) (LSet.diff levels named) ((pl,0),univs) in - Lib.add_anonymous_leaf (input_univ_names (QualifiedUniv l, univs)) + input_univ_names (QualifiedUniv l, univs) let do_universe ~poly l = let in_section = Global.sections_are_opened () in @@ -134,7 +138,7 @@ let do_universe ~poly l = Univ.LSet.empty l, Univ.Constraint.empty in let src = if poly then BoundUniv else UnqualifiedUniv in - let () = Lib.add_anonymous_leaf (input_univ_names (src, l)) in + let () = input_univ_names (src, l) in DeclareUctx.declare_universe_context ~poly ctx let do_constraint ~poly l = |