Merge PR #890: Global universe declarations

1 files changed, 66 insertions, 62 deletions

diff --git a/API/API.mli b/API/API.mli
index e320e496c0..6227f17c65 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -1861,6 +1861,60 @@ end
 (* Modules from intf/                                                   *)
 (************************************************************************)
 
+module Libnames :
+sig
+
+  open Util
+  open Names
+
+  type full_path
+  val pr_path : full_path -> Pp.t
+  val make_path : Names.DirPath.t -> Names.Id.t -> full_path
+  val eq_full_path : full_path -> full_path -> bool
+  val repr_path : full_path -> Names.DirPath.t * Names.Id.t
+  val dirpath : full_path -> Names.DirPath.t
+  val path_of_string : string -> full_path
+
+  type qualid
+  val make_qualid : Names.DirPath.t -> Names.Id.t -> qualid
+  val qualid_eq : qualid -> qualid -> bool
+  val repr_qualid : qualid -> Names.DirPath.t * Names.Id.t
+  val pr_qualid : qualid -> Pp.t
+  val string_of_qualid : qualid -> string
+  val qualid_of_string : string -> qualid
+  val qualid_of_path : full_path -> qualid
+  val qualid_of_dirpath : Names.DirPath.t -> qualid
+  val qualid_of_ident : Names.Id.t -> qualid
+
+  type reference =
+    | Qualid of qualid Loc.located
+    | Ident of Names.Id.t Loc.located
+  val loc_of_reference : reference -> Loc.t option
+  val qualid_of_reference : reference -> qualid Loc.located
+  val pr_reference : reference -> Pp.t
+
+  val is_dirpath_prefix_of : Names.DirPath.t -> Names.DirPath.t -> bool
+  val split_dirpath : Names.DirPath.t -> Names.DirPath.t * Names.Id.t
+  val dirpath_of_string : string -> Names.DirPath.t
+  val pr_dirpath : Names.DirPath.t -> Pp.t
+  [@@ocaml.deprecated "Alias for DirPath.print"]
+
+  val string_of_path : full_path -> string
+
+  val basename : full_path -> Names.Id.t
+
+  type object_name = full_path * Names.KerName.t
+  type object_prefix = {
+    obj_dir : DirPath.t;
+    obj_mp  : ModPath.t;
+    obj_sec : DirPath.t;
+  }
+
+  module Dirset : Set.S with type elt = DirPath.t
+  module Dirmap : Map.ExtS with type key = DirPath.t and module Set := Dirset
+  module Spmap  : CSig.MapS with type key = full_path
+end
+
 module Misctypes :
 sig
   type evars_flag = bool
@@ -1883,10 +1937,15 @@ sig
     | GSet  (** representation of [Set] literal *)
     | GType of 'a (** representation of [Type] literal *)
 
-  type level_info = Names.Name.t Loc.located option
+  type 'a universe_kind =
+    | UAnonymous
+    | UUnknown
+    | UNamed of 'a
+
+  type level_info = Libnames.reference universe_kind
   type glob_level = level_info glob_sort_gen
 
-  type sort_info = Names.Name.t Loc.located list
+  type sort_info = (Libnames.reference * int) option list
   type glob_sort = sort_info glob_sort_gen
 
   type ('a, 'b) gen_universe_decl = {
@@ -2039,60 +2098,6 @@ sig
   [@@ocaml.deprecated "alias of API.Names"]
 end
 
-module Libnames :
-sig
-
-  open Util
-  open Names
-
-  type full_path
-  val pr_path : full_path -> Pp.t
-  val make_path : Names.DirPath.t -> Names.Id.t -> full_path
-  val eq_full_path : full_path -> full_path -> bool
-  val repr_path : full_path -> Names.DirPath.t * Names.Id.t
-  val dirpath : full_path -> Names.DirPath.t
-  val path_of_string : string -> full_path
-
-  type qualid
-  val make_qualid : Names.DirPath.t -> Names.Id.t -> qualid
-  val qualid_eq : qualid -> qualid -> bool
-  val repr_qualid : qualid -> Names.DirPath.t * Names.Id.t
-  val pr_qualid : qualid -> Pp.t
-  val string_of_qualid : qualid -> string
-  val qualid_of_string : string -> qualid
-  val qualid_of_path : full_path -> qualid
-  val qualid_of_dirpath : Names.DirPath.t -> qualid
-  val qualid_of_ident : Names.Id.t -> qualid
-
-  type reference =
-    | Qualid of qualid Loc.located
-    | Ident of Names.Id.t Loc.located
-  val loc_of_reference : reference -> Loc.t option
-  val qualid_of_reference : reference -> qualid Loc.located
-  val pr_reference : reference -> Pp.t
-
-  val is_dirpath_prefix_of : Names.DirPath.t -> Names.DirPath.t -> bool
-  val split_dirpath : Names.DirPath.t -> Names.DirPath.t * Names.Id.t
-  val dirpath_of_string : string -> Names.DirPath.t
-  val pr_dirpath : Names.DirPath.t -> Pp.t
-  [@@ocaml.deprecated "Alias for DirPath.print"]
-
-  val string_of_path : full_path -> string
-
-  val basename : full_path -> Names.Id.t
-
-  type object_name = full_path * Names.KerName.t
-  type object_prefix = {
-    obj_dir : DirPath.t;
-    obj_mp  : ModPath.t;
-    obj_sec : DirPath.t;
-  }
-
-  module Dirset : Set.S with type elt = DirPath.t
-  module Dirmap : Map.ExtS with type key = DirPath.t and module Set := Dirset
-  module Spmap  : CSig.MapS with type key = full_path
-end
-
 module Globnames :
 sig
 
@@ -2754,10 +2759,10 @@ sig
   type universe_binders
   type universe_opt_subst
   val fresh_inductive_instance : Environ.env -> Names.inductive -> Constr.pinductive Univ.in_universe_context_set
-  val new_Type : Names.DirPath.t -> Constr.types
+  val new_Type : unit -> Constr.types
   val type_of_global : Globnames.global_reference -> Constr.types Univ.in_universe_context_set
   val constr_of_global : Globnames.global_reference -> Constr.t
-  val new_univ_level : Names.DirPath.t -> Univ.Level.t
+  val new_univ_level : unit -> Univ.Level.t
   val new_sort_in_family : Sorts.family -> Sorts.t
   val pr_with_global_universes : Univ.Level.t -> Pp.t
   val pr_universe_opt_subst : universe_opt_subst -> Pp.t
@@ -4842,17 +4847,16 @@ sig
       set : unit -> unit ;
       reset : unit -> unit
     }
-  type proof_universes = UState.t * Universes.universe_binders option
   type proof_object = {
     id : Names.Id.t;
     entries : Safe_typing.private_constants Entries.definition_entry list;
     persistence : Decl_kinds.goal_kind;
-    universes: proof_universes;
+    universes: UState.t;
   }
 
   type proof_ending =
   | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry *
-                  proof_universes
+                  UState.t
   | Proved of Vernacexpr.opacity_flag *
               Vernacexpr.lident option *
               proof_object
@@ -5006,7 +5010,7 @@ sig
       Vernacexpr.goal_selector -> int option -> unit Proofview.tactic ->
       Proof.t -> Proof.t * bool
   val cook_proof :
-    unit -> (Names.Id.t * (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * Decl_kinds.goal_kind))
+    unit -> (Names.Id.t * (Safe_typing.private_constants Entries.definition_entry * UState.t * Decl_kinds.goal_kind))
 
   val get_current_context : unit -> Evd.evar_map * Environ.env
   val current_proof_statement : unit -> Names.Id.t * Decl_kinds.goal_kind * EConstr.types