diff options
Diffstat (limited to 'engine/univGen.mli')
| -rw-r--r-- | engine/univGen.mli | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/engine/univGen.mli b/engine/univGen.mli index 66e80368a4..b4598e10d0 100644 --- a/engine/univGen.mli +++ b/engine/univGen.mli @@ -15,11 +15,13 @@ open Univ (** The global universe counter *) -val set_remote_new_univ_id : Level.Id.t RemoteCounter.installer +type univ_unique_id +val set_remote_new_univ_id : univ_unique_id RemoteCounter.installer +val new_univ_id : unit -> univ_unique_id (** for the stm *) (** Side-effecting functions creating new universe levels. *) -val new_univ_id : unit -> Level.Id.t +val new_univ_global : unit -> Level.UGlobal.t val fresh_level : unit -> Level.t val new_univ : unit -> Universe.t |