diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-07-01 22:50:37 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-07-01 22:52:08 +0200 |
| commit | 4c97e4ce19ca4c387039cfdcb4f24658100230b0 (patch) | |
| tree | 8e6367b1936d842b3e56283abc25de2342452884 /library/universes.mli | |
| parent | 3d2582eeb492fb21b7136016bf4c1a0463dc15c2 (diff) | |
Add toplevel commands to declare global universes and constraints.
Diffstat (limited to 'library/universes.mli')
| -rw-r--r-- | library/universes.mli | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/library/universes.mli b/library/universes.mli index 691f404aa..5b0951928 100644 --- a/library/universes.mli +++ b/library/universes.mli @@ -17,6 +17,12 @@ open Univ (** Universes *) +type universe_names = + Univ.universe_level Idmap.t * Id.t Univ.LMap.t + +val global_universe_names : unit -> universe_names +val set_global_universe_names : universe_names -> unit + (** The global universe counter *) val set_remote_new_univ_level : universe_level RemoteCounter.installer @@ -237,4 +243,3 @@ val minimize_univ_variables : Univ.LSet.t * Univ.universe option Univ.LMap.t * Univ.LSet.t * (bool * bool * Univ.universe) Univ.LMap.t * Univ.constraints - |