diff options
-rw-r--r-- | engine/engine.mllib | 1 | ||||
-rw-r--r-- | engine/universes.ml (renamed from library/universes.ml) | 13 | ||||
-rw-r--r-- | engine/universes.mli (renamed from library/universes.mli) | 7 | ||||
-rw-r--r-- | library/declare.ml | 6 | ||||
-rw-r--r-- | library/global.ml | 12 | ||||
-rw-r--r-- | library/global.mli | 7 | ||||
-rw-r--r-- | library/library.mllib | 1 | ||||
-rw-r--r-- | pretyping/pretyping.ml | 2 |
8 files changed, 25 insertions, 24 deletions
diff --git a/engine/engine.mllib b/engine/engine.mllib index 9cc6d9109..53cbbd73e 100644 --- a/engine/engine.mllib +++ b/engine/engine.mllib @@ -1,5 +1,6 @@ Logic_monad Namegen +Universes UState Evd Sigma diff --git a/library/universes.ml b/engine/universes.ml index 0ccb6b8d2..6d683b859 100644 --- a/library/universes.ml +++ b/engine/universes.ml @@ -15,19 +15,8 @@ open Univ open Globnames open Decl_kinds -(** Global universe names *) -type universe_names = - (polymorphic * 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 - let pr_with_global_universes l = - try Nameops.pr_id (LMap.find l (snd !global_universes)) + try Nameops.pr_id (LMap.find l (snd (Global.global_universe_names ()))) with Not_found -> Level.pr l (** Local universe names of polymorphic references *) diff --git a/library/universes.mli b/engine/universes.mli index d3a271b8d..0aeea91cd 100644 --- a/library/universes.mli +++ b/engine/universes.mli @@ -17,13 +17,6 @@ val is_set_minimization : unit -> bool (** Universes *) -(** Global universe name <-> level mapping *) -type universe_names = - (Decl_kinds.polymorphic * 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 - val pr_with_global_universes : Level.t -> Pp.std_ppcmds (** Local universe name <-> level mapping *) diff --git a/library/declare.ml b/library/declare.ml index 8298ddbc8..31c9c24bc 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -455,7 +455,7 @@ let declare_universe_context poly ctx = type universe_decl = polymorphic * (Id.t * Univ.universe_level) list let cache_universes (p, l) = - let glob = Universes.global_universe_names () in + let glob = Global.global_universe_names () in let glob', ctx = List.fold_left (fun ((idl,lid),ctx) (id, lev) -> ((Idmap.add id (p, lev) idl, @@ -464,7 +464,7 @@ let cache_universes (p, l) = (glob, Univ.ContextSet.empty) l in cache_universe_context (p, ctx); - Universes.set_global_universe_names glob' + Global.set_global_universe_names glob' let input_universes : universe_decl -> Libobject.obj = declare_object @@ -519,7 +519,7 @@ let do_constraint poly l = (str "Cannot declare constraints on anonymous universes") | GType (Some (loc, id)) -> let id = Id.of_string id in - let names, _ = Universes.global_universe_names () in + let names, _ = Global.global_universe_names () in try loc, Idmap.find id names with Not_found -> user_err ~loc ~hdr:"Constraint" (str "Undeclared universe " ++ pr_id id) diff --git a/library/global.ml b/library/global.ml index e748434d2..5fa710b36 100644 --- a/library/global.ml +++ b/library/global.ml @@ -8,6 +8,7 @@ open Names open Environ +open Decl_kinds (** We introduce here the global environment of the system, and we declare it as a synchronized table. *) @@ -229,6 +230,17 @@ let universes_of_global env r = let universes_of_global gr = universes_of_global (env ()) gr +(** Global universe names *) +type universe_names = + (polymorphic * 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 + let is_polymorphic r = let env = env() in match r with diff --git a/library/global.mli b/library/global.mli index 247ca20b4..a4a38ce84 100644 --- a/library/global.mli +++ b/library/global.mli @@ -96,6 +96,13 @@ val constraints_of_constant_body : val universes_of_constant_body : Declarations.constant_body -> Univ.universe_context +(** Global universe name <-> level mapping *) +type universe_names = + (Decl_kinds.polymorphic * 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 + (** {6 Compiled libraries } *) val start_library : DirPath.t -> module_path diff --git a/library/library.mllib b/library/library.mllib index 920657365..df4f73503 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -5,7 +5,6 @@ Libobject Summary Nametab Global -Universes Lib Declaremods Loadpath diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 2f13121ad..8f369a811 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -188,7 +188,7 @@ let _ = (** Miscellaneous interpretation functions *) let interp_universe_level_name evd (loc,s) = - let names, _ = Universes.global_universe_names () in + let names, _ = Global.global_universe_names () in if CString.string_contains s "." then match List.rev (CString.split '.' s) with | [] -> anomaly (str"Invalid universe name " ++ str s) |