From 20c98eab851210702b39e1c66e005acfc351d8dd Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 1 Dec 2017 10:11:41 +0100
Subject: Proper nametab handling of global universe names

They are now bound at the library + module level and can be qualified
and shadowed according to the usual rules of qualified names.
Parsing and printing of universes "u+n" done as well.
In sections, global universes are discharged as well, checking that
they can be defined globally when they are introduced
---
 API/API.mli | 121 +++++++++++++++++++++++++++++++-----------------------------
 1 file changed, 63 insertions(+), 58 deletions(-)

(limited to 'API/API.mli')

diff --git a/API/API.mli b/API/API.mli
index e320e496c0..9d1585d602 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
-- 
cgit v1.2.3


From 4fcf1fa32ff395d6bd5f6ce4803eee18173c4d36 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 22 Nov 2017 18:39:34 +0100
Subject: Cleanup API for registering universe binders.

- Regularly declared for for polymorphic constants
- Declared globally for monomorphic constants.

  E.g mono@{i} := Type@{i} is printed as
  mono@{mono.i} := Type@{mono.i}.

  There can be a name clash if there's a module and a constant of the
  same name. It is detected and is an error if the constant is first
  but is not detected and the name for the constant not
  registered (??) if the constant comes second.

Accept VarRef when registering universe binders

Fix two problems found by Gaëtan where binders were not registered properly

Simplify API substantially by not passing around a substructure of an
already carrier-around structure in interpretation/declaration code of
constants and proofs

Fix an issue of the stronger restrict universe context + no evd leak

This is uncovered by not having an evd leak in interp_definition, and
the stronger restrict_universe_context. This patch could be backported
to 8.7, it could also be triggered by the previous restrict_context I
think.
---
 API/API.mli | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'API/API.mli')

diff --git a/API/API.mli b/API/API.mli
index 9d1585d602..6227f17c65 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -4847,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
@@ -5011,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
-- 
cgit v1.2.3