From da049e138e2b1acf9cdd40d3dbac4508f76f21cb Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 10 Oct 2018 14:08:08 +0200
Subject: Deprecate UnivGen.new_{univ,Type,Type_sort}

They are impractical since we need to get the level out to register it
afterwards.
---
 engine/univGen.mli | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'engine')

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
-- 
cgit v1.2.3