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.ml | |
| parent | 3d2582eeb492fb21b7136016bf4c1a0463dc15c2 (diff) | |
Add toplevel commands to declare global universes and constraints.
Diffstat (limited to 'library/universes.ml')
| -rw-r--r-- | library/universes.ml | 10 |
1 files changed, 10 insertions, 0 deletions
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 |