From 4c97e4ce19ca4c387039cfdcb4f24658100230b0 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 1 Jul 2014 22:50:37 +0200 Subject: Add toplevel commands to declare global universes and constraints. --- library/universes.mli | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'library/universes.mli') 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 - -- cgit v1.2.3