diff options
| author | Gaëtan Gilbert | 2018-12-06 15:52:37 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-12-06 17:10:02 +0100 |
| commit | cff3c5a7148afc722852bd01658fe49ffec1d967 (patch) | |
| tree | 63a70acbd8a9657040461fd2fc06b51e0ee960df /engine/univGen.mli | |
| parent | 3e275d4bd1c3eb002b68c36ab116e5ab687d52f3 (diff) | |
Revise API for global universes.
Rename Univ.Level.{Qualid -> UGlobal}, remove Univ.Level.Id.
Remove the ability to split the argument of `Univ.Level.Level` into a
dirpath*int pair (except by going through string hacks like
detyping/pretyping(/funind) does).
Id.of_string_soft to turn unnamed universes into qualid is pushed up
to detyping. (TODO some followup PR clean up more)
This makes it pointless to have an opaque type for ints in
Univ.Level: it would only be used as argument to
Univ.Level.UGlobal.make, ie
~~~
open Univ.Level
let x = UGlobal.make dp (Id.make n)
(* vs *)
let x = UGlobal.make dp n
~~~
Remaining places which create levels from ints are various hacks (eg
the dummy in inductive.ml, the Type.n universes in ugraph
sort_universes) and univgen.
UnivGen does have an opaque type for ints used as univ ids since they
get manipulated by the stm.
NB: build breaks due to ocamldep issue if UGlobal is named Global instead.
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 |