diff options
| author | Gaëtan Gilbert | 2018-10-10 14:08:08 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-10-16 15:52:53 +0200 |
| commit | da049e138e2b1acf9cdd40d3dbac4508f76f21cb (patch) | |
| tree | d3fc16c340bece88e617f716cbf16637578afa63 /engine | |
| parent | bab144fed76c452c49c95c87682d442df68b82f2 (diff) | |
Deprecate UnivGen.new_{univ,Type,Type_sort}
They are impractical since we need to get the level out to register it
afterwards.
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/univGen.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/engine/univGen.mli b/engine/univGen.mli index cc3803f393..136c04f969 100644 --- a/engine/univGen.mli +++ b/engine/univGen.mli @@ -23,9 +23,13 @@ val set_remote_new_univ_id : universe_id RemoteCounter.installer val new_univ_id : unit -> universe_id val new_univ_level : unit -> Level.t + val new_univ : unit -> Universe.t +[@@ocaml.deprecated "Use [new_univ_level]"] val new_Type : unit -> types +[@@ocaml.deprecated "Use [new_univ_level]"] val new_Type_sort : unit -> Sorts.t +[@@ocaml.deprecated "Use [new_univ_level]"] val new_global_univ : unit -> Universe.t in_universe_context_set val new_sort_in_family : Sorts.family -> Sorts.t |