diff options
| author | Gaëtan Gilbert | 2018-09-14 12:59:52 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-09-27 13:28:33 +0200 |
| commit | 2566d45fcc05c1cd80ba2ac16ef342e7f145f01a (patch) | |
| tree | da9b8f3d9574f467ae494dba4acb703f726c06c9 /engine/universes.mli | |
| parent | 49e9fe1c4666beda099872988144d12138dc6349 (diff) | |
Fix #8478: Undeclared universe anomaly with sections
Instead of looking into the name-oriented structure we look into the
actual section structures.
Note: together with #8475 this lets us remove UnivNames.add_global_universe.
Diffstat (limited to 'engine/universes.mli')
| -rw-r--r-- | engine/universes.mli | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/engine/universes.mli b/engine/universes.mli index 7ca33f47a1..0d3bae4c95 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -25,12 +25,6 @@ val pr_with_global_universes : Level.t -> Pp.t val reference_of_level : Level.t -> Libnames.qualid [@@ocaml.deprecated "Use [UnivNames.qualid_of_level]"] -val add_global_universe : Level.t -> Decl_kinds.polymorphic -> unit -[@@ocaml.deprecated "Use [UnivNames.add_global_universe]"] - -val is_polymorphic : Level.t -> bool -[@@ocaml.deprecated "Use [UnivNames.is_polymorphic]"] - type universe_binders = UnivNames.universe_binders [@@ocaml.deprecated "Use [UnivNames.universe_binders]"] |