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.ml | 10 ++++++++++ 1 file changed, 10 insertions(+) (limited to 'library/universes.ml') diff --git a/library/universes.ml b/library/universes.ml index 0699326c5..e84f1f975 100644 --- a/library/universes.ml +++ b/library/universes.ml @@ -13,6 +13,16 @@ open Term open Environ open Univ +type universe_names = + Univ.universe_level Idmap.t * Id.t Univ.LMap.t + +let global_universes = Summary.ref ~name:"Global universe names" + ((Idmap.empty, Univ.LMap.empty) : universe_names) + +let global_universe_names () = !global_universes +let set_global_universe_names s = global_universes := s + + type universe_constraint_type = ULe | UEq | ULub type universe_constraint = universe * universe_constraint_type * universe -- cgit v1.2.3