[api] Rename global_reference to GlobRef.t to follow kernel style.

In coq#6092, `global_reference` was moved to `kernel`. It makes sense to
go further and use the current kernel style for names.

This has a good effect on the dependency graph, as some core modules
don't depend on library anymore.

A question about providing equality for the GloRef module remains, as
there are two different notions of equality for constants. In that
sense, `KerPair` seems suspicious and at some point it should be
looked at.

dev/doc/changes.md

@@ -4,7 +4,7 @@
 
 Proof engine
 
-  More functions have been changed to use `EConstr`, notably the
+- More functions have been changed to use `EConstr`, notably the
   functions in `Evd`, and in particular `Evd.define`.
 
   Note that the core function `EConstr.to_constr` now _enforces_ by
@@ -18,6 +18,10 @@ Proof engine
   that setting this flag to false is deprecated so it is only meant to
   be used as to help port pre-EConstr code.
 
+- A few type alias have been deprecated, in all cases the message
+  should indicate what the canonical form is. An important change is
+  the move of `Globnames.global_reference` to `Names.GlobRef.t`.
+
 ## Changes between Coq 8.7 and Coq 8.8
 
 ### Bug tracker
@@ -94,6 +98,11 @@ Declaration of printers for arguments used only in vernac command
   happen. An alternative is to register the corresponding argument as
   a value, using "Geninterp.register_val0 wit None".
 
+Types Alias deprecation and type relocation.
+
+- A few type alias have been deprecated, in all cases the message
+  should indicate what the canonical form is.
+
 ### STM API
 
 The STM API has seen a general overhaul. The main change is the

dev/top_printers.mli

@@ -87,7 +87,7 @@ val ppclosedglobconstr : Ltac_pretype.closed_glob_constr -> unit
 val ppclosedglobconstridmap :
   Ltac_pretype.closed_glob_constr Names.Id.Map.t -> unit
 
-val ppglobal : Globnames.global_reference -> unit
+val ppglobal : Names.GlobRef.t -> unit
 
 val ppconst :
   Names.KerName.t * (Constr.constr, 'a) Environ.punsafe_judgment -> unit

engine/eConstr.ml

@@ -500,6 +500,7 @@ let eq_universes env sigma cstrs cv_pb ref nargs l l' =
     let l = Evd.normalize_universe_instance sigma l
     and l' = Evd.normalize_universe_instance sigma l' in
     let open Universes in
+    let open GlobRef in
     match ref with
     | VarRef _ -> assert false (* variables don't have instances *)
     | ConstRef _ ->

engine/eConstr.mli

@@ -284,9 +284,9 @@ val map_rel_context_in_env :
 (* XXX Missing Sigma proxy *)
 val fresh_global :
   ?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env ->
-  Evd.evar_map -> Globnames.global_reference -> Evd.evar_map * t
+  Evd.evar_map -> GlobRef.t -> Evd.evar_map * t
 
-val is_global : Evd.evar_map -> Globnames.global_reference -> t -> bool
+val is_global : Evd.evar_map -> GlobRef.t -> t -> bool
 
 (** {5 Extra} *)
 

engine/evar_kinds.ml

@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Names
-open Globnames
 open Misctypes
 
 (** The kinds of existential variable *)
@@ -24,7 +23,7 @@ type matching_var_kind = FirstOrderPatVar of patvar | SecondOrderPatVar of patva
 type subevar_kind = Domain | Codomain | Body
 
 type t =
-  | ImplicitArg of global_reference * (int * Id.t option)
+  | ImplicitArg of GlobRef.t * (int * Id.t option)
      * bool (** Force inference *)
   | BinderType of Name.t
   | NamedHole of Id.t (* coming from some ?[id] syntax *)

engine/evarutil.ml

@@ -534,7 +534,7 @@ type clear_dependency_error =
 | OccurHypInSimpleClause of Id.t option
 | EvarTypingBreak of existential
 
-exception ClearDependencyError of Id.t * clear_dependency_error * Globnames.global_reference option
+exception ClearDependencyError of Id.t * clear_dependency_error * GlobRef.t option
 
 exception Depends of Id.t
 

engine/evarutil.mli

@@ -78,8 +78,8 @@ val restrict_evar : evar_map -> Evar.t -> Filter.t ->
 
 (** Polymorphic constants *)
 
-val new_global : evar_map -> Globnames.global_reference -> evar_map * constr
-val e_new_global : evar_map ref -> Globnames.global_reference -> constr
+val new_global : evar_map -> GlobRef.t -> evar_map * constr
+val e_new_global : evar_map ref -> GlobRef.t -> constr
 
 (** Create a fresh evar in a context different from its definition context:
    [new_evar_instance sign evd ty inst] creates a new evar of context
@@ -235,7 +235,7 @@ type clear_dependency_error =
 | OccurHypInSimpleClause of Id.t option
 | EvarTypingBreak of Constr.existential
 
-exception ClearDependencyError of Id.t * clear_dependency_error * Globnames.global_reference option
+exception ClearDependencyError of Id.t * clear_dependency_error * GlobRef.t option
 
 val clear_hyps_in_evi : env -> evar_map ref -> named_context_val -> types ->
   Id.Set.t -> named_context_val * types

engine/evd.mli

@@ -649,7 +649,7 @@ val fresh_inductive_instance : ?loc:Loc.t -> env -> evar_map -> inductive -> eva
 val fresh_constructor_instance : ?loc:Loc.t -> env -> evar_map -> constructor -> evar_map * pconstructor
 
 val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> env ->
-  evar_map -> Globnames.global_reference -> evar_map * econstr
+  evar_map -> GlobRef.t -> evar_map * econstr
 
 (********************************************************************)
 (* constr with holes and pending resolution of classes, conversion  *)

engine/termops.mli

@@ -112,7 +112,7 @@ val dependent_in_decl : Evd.evar_map -> constr -> named_declaration -> bool
 val count_occurrences : Evd.evar_map -> constr -> constr -> int
 val collect_metas : Evd.evar_map -> constr -> int list
 val collect_vars : Evd.evar_map -> constr -> Id.Set.t (** for visible vars only *)
-val vars_of_global_reference : env -> Globnames.global_reference -> Id.Set.t
+val vars_of_global_reference : env -> GlobRef.t -> Id.Set.t
 val occur_term : Evd.evar_map -> constr -> constr -> bool (** Synonymous of dependent *)
 [@@ocaml.deprecated "alias of Termops.dependent"]
 
@@ -261,7 +261,7 @@ val clear_named_body : Id.t -> env -> env
 val global_vars : env -> Evd.evar_map -> constr -> Id.t list
 val global_vars_set : env -> Evd.evar_map -> constr -> Id.Set.t
 val global_vars_set_of_decl : env -> Evd.evar_map -> named_declaration -> Id.Set.t
-val global_app_of_constr : Evd.evar_map -> constr -> (Globnames.global_reference * EInstance.t) * constr option
+val global_app_of_constr : Evd.evar_map -> constr -> (GlobRef.t * EInstance.t) * constr option
 
 (** Gives an ordered list of hypotheses, closed by dependencies,
    containing a given set *)
@@ -270,9 +270,9 @@ val dependency_closure : env -> Evd.evar_map -> named_context -> Id.Set.t -> Id.
 (** Test if an identifier is the basename of a global reference *)
 val is_section_variable : Id.t -> bool
 
-val global_of_constr : Evd.evar_map -> constr -> Globnames.global_reference * EInstance.t
+val global_of_constr : Evd.evar_map -> constr -> GlobRef.t * EInstance.t
 
-val is_global : Evd.evar_map -> Globnames.global_reference -> constr -> bool
+val is_global : Evd.evar_map -> GlobRef.t -> constr -> bool
 
 val isGlobalRef : Evd.evar_map -> constr -> bool
 

engine/universes.ml

@@ -74,7 +74,7 @@ let subst_ubinder (subst,(ref,l as orig)) =
 let discharge_ubinder (_,(ref,l)) =
   Some (Lib.discharge_global ref, l)
 
-let ubinder_obj : Globnames.global_reference * universe_binders -> Libobject.obj =
+let ubinder_obj : GlobRef.t * universe_binders -> Libobject.obj =
   let open Libobject in
   declare_object { (default_object "universe binder") with
     cache_function = cache_ubinder;

engine/universes.mli

@@ -37,8 +37,8 @@ type universe_binders = Univ.Level.t Names.Id.Map.t
 
 val empty_binders : universe_binders
 
-val register_universe_binders : Globnames.global_reference -> universe_binders -> unit
-val universe_binders_of_global : Globnames.global_reference -> universe_binders
+val register_universe_binders : GlobRef.t -> universe_binders -> unit
+val universe_binders_of_global : GlobRef.t -> universe_binders
 
 type univ_name_list = Misctypes.lname list
 
@@ -48,7 +48,7 @@ type univ_name_list = Misctypes.lname list
     May error if the lengths mismatch.
 
     Otherwise return [universe_binders_of_global ref]. *)
-val universe_binders_with_opt_names : Globnames.global_reference ->
+val universe_binders_with_opt_names : Names.GlobRef.t ->
   Univ.Level.t list -> univ_name_list option -> universe_binders
 
 (** The global universe counter *)
@@ -132,7 +132,7 @@ val fresh_inductive_instance : env -> inductive ->
 val fresh_constructor_instance : env -> constructor ->
   pconstructor in_universe_context_set
 
-val fresh_global_instance : ?names:Univ.Instance.t -> env -> Globnames.global_reference -> 
+val fresh_global_instance : ?names:Univ.Instance.t -> env -> GlobRef.t ->
   constr in_universe_context_set
 
 val fresh_global_or_constr_instance : env -> Globnames.global_reference_or_constr -> 
@@ -144,9 +144,9 @@ val fresh_universe_context_set_instance : ContextSet.t ->
   universe_level_subst * ContextSet.t
 
 (** Raises [Not_found] if not a global reference. *)
-val global_of_constr : constr -> Globnames.global_reference puniverses
+val global_of_constr : constr -> GlobRef.t puniverses
 
-val constr_of_global_univ : Globnames.global_reference puniverses -> constr
+val constr_of_global_univ : GlobRef.t puniverses -> constr
 
 val extend_context : 'a in_universe_context_set -> ContextSet.t -> 
   'a in_universe_context_set
@@ -204,16 +204,16 @@ val normalize_universe_subst : universe_subst ref ->
     the constraints should be properly added to an evd. 
     See Evd.fresh_global, Evarutil.new_global, and pf_constr_of_global for
     the proper way to get a fresh copy of a global reference. *)
-val constr_of_global : Globnames.global_reference -> constr
+val constr_of_global : GlobRef.t -> constr
 
 (** ** DEPRECATED ** synonym of [constr_of_global] *)
-val constr_of_reference : Globnames.global_reference -> constr
+val constr_of_reference : GlobRef.t -> constr
 [@@ocaml.deprecated "synonym of [constr_of_global]"]
 
 (** Returns the type of the global reference, by creating a fresh instance of polymorphic 
     references and computing their instantiated universe context. (side-effect on the
     universe counter, use with care). *)
-val type_of_global : Globnames.global_reference -> types in_universe_context_set
+val type_of_global : GlobRef.t -> types in_universe_context_set
 
 (** Full universes substitutions into terms *)
 

interp/constrextern.mli

@@ -13,7 +13,6 @@ open Termops
 open EConstr
 open Environ
 open Libnames
-open Globnames
 open Glob_term
 open Pattern
 open Constrexpr
@@ -40,7 +39,7 @@ val extern_closed_glob : ?lax:bool -> bool -> env -> Evd.evar_map -> closed_glob
 
 val extern_constr : ?lax:bool -> bool -> env -> Evd.evar_map -> constr -> constr_expr
 val extern_constr_in_scope : bool -> scope_name -> env -> Evd.evar_map -> constr -> constr_expr
-val extern_reference : ?loc:Loc.t -> Id.Set.t -> global_reference -> reference
+val extern_reference : ?loc:Loc.t -> Id.Set.t -> GlobRef.t -> reference
 val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr
 val extern_sort : Evd.evar_map -> Sorts.t -> glob_sort
 val extern_rel_context : constr option -> env -> Evd.evar_map ->
@@ -58,9 +57,9 @@ val print_projections : bool ref
 
 (** Customization of the global_reference printer *)
 val set_extern_reference :
-  (?loc:Loc.t -> Id.Set.t -> global_reference -> reference) -> unit
+  (?loc:Loc.t -> Id.Set.t -> GlobRef.t -> reference) -> unit
 val get_extern_reference :
-  unit -> (?loc:Loc.t -> Id.Set.t -> global_reference -> reference)
+  unit -> (?loc:Loc.t -> Id.Set.t -> GlobRef.t -> reference)
 
 (** WARNING: The following functions are evil due to
     side-effects. Think of the following case as used in the printer:

interp/constrintern.ml

@@ -1077,7 +1077,7 @@ let interp_reference vars r =
 (** Private internalization patterns *)
 type 'a raw_cases_pattern_expr_r =
   | RCPatAlias of 'a raw_cases_pattern_expr * Misctypes.lname
-  | RCPatCstr  of Globnames.global_reference
+  | RCPatCstr  of GlobRef.t
     * 'a raw_cases_pattern_expr list * 'a raw_cases_pattern_expr list
   (** [RCPatCstr (loc, c, l1, l2)] represents [((@ c l1) l2)] *)
   | RCPatAtom  of (Misctypes.lident * (Notation_term.tmp_scope_name option * Notation_term.scope_name list)) option
@@ -1314,7 +1314,7 @@ let sort_fields ~complete loc fields completer =
               | [] -> (idx, acc_first_idx, acc)
               | (Some field_glob_id) :: projs ->
                  let field_glob_ref = ConstRef field_glob_id in
-                 let first_field = eq_gr field_glob_ref first_field_glob_ref in
+                 let first_field = GlobRef.equal field_glob_ref first_field_glob_ref in
                  begin match proj_kinds with
                     | [] -> anomaly (Pp.str "Number of projections mismatch.")
                     | (_, regular) :: proj_kinds ->
@@ -1352,7 +1352,7 @@ let sort_fields ~complete loc fields completer =
                  user_err ?loc ~hdr:"intern"
                                (str "The field \"" ++ pr_reference field_ref ++ str "\" does not exist.") in
                let remaining_projs, (field_index, _) =
-                 let the_proj (idx, glob_id) = eq_gr field_glob_ref (ConstRef glob_id) in
+                 let the_proj (idx, glob_id) = GlobRef.equal field_glob_ref (ConstRef glob_id) in
                  try CList.extract_first the_proj remaining_projs
                  with Not_found ->
                    user_err ?loc 

interp/constrintern.mli

@@ -13,7 +13,6 @@ open Evd
 open Environ
 open Misctypes
 open Libnames
-open Globnames
 open Glob_term
 open Pattern
 open EConstr
@@ -143,7 +142,7 @@ val intern_constr_pattern :
     constr_pattern_expr -> patvar list * constr_pattern
 
 (** Raise Not_found if syndef not bound to a name and error if unexisting ref *)
-val intern_reference : reference -> global_reference
+val intern_reference : reference -> GlobRef.t
 
 (** Expands abbreviations (syndef); raise an error if not existing *)
 val interp_reference : ltac_sign -> reference -> glob_constr
@@ -175,11 +174,11 @@ val interp_context_evars :
 (** Locating references of constructions, possibly via a syntactic definition 
    (these functions do not modify the glob file) *)
 
-val locate_reference :  Libnames.qualid -> Globnames.global_reference
+val locate_reference :  Libnames.qualid -> GlobRef.t
 val is_global : Id.t -> bool
-val construct_reference : ('c, 't) Context.Named.pt -> Id.t -> Globnames.global_reference
-val global_reference : Id.t -> Globnames.global_reference
-val global_reference_in_absolute_module : DirPath.t -> Id.t -> Globnames.global_reference
+val construct_reference : ('c, 't) Context.Named.pt -> Id.t -> GlobRef.t
+val global_reference : Id.t -> GlobRef.t
+val global_reference_in_absolute_module : DirPath.t -> Id.t -> GlobRef.t
 
 (** Interprets a term as the left-hand side of a notation. The returned map is
     guaranteed to have the same domain as the input one. *)

interp/declare.mli

@@ -83,7 +83,7 @@ val recursive_message : bool (** true = fixpoint *) ->
 val exists_name : Id.t -> bool
 
 (** Global universe contexts, names and constraints *)
-val declare_univ_binders : Globnames.global_reference -> Universes.universe_binders -> unit
+val declare_univ_binders : GlobRef.t -> Universes.universe_binders -> unit
 
 val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit
 

interp/dumpglob.mli

@@ -24,7 +24,7 @@ val feedback_glob : unit -> unit
 val pause : unit -> unit
 val continue : unit -> unit
 
-val add_glob : ?loc:Loc.t -> Globnames.global_reference -> unit
+val add_glob : ?loc:Loc.t -> Names.GlobRef.t -> unit
 val add_glob_kn : ?loc:Loc.t -> Names.KerName.t -> unit
 
 val dump_definition : Misctypes.lident -> bool -> string -> unit
@@ -43,4 +43,4 @@ val dump_constraint :
 
 val dump_string : string -> unit
 
-val type_of_global_ref : Globnames.global_reference -> string 
+val type_of_global_ref : Names.GlobRef.t -> string

interp/impargs.ml

@@ -505,7 +505,7 @@ type implicit_discharge_request =
   | ImplLocal
   | ImplConstant of Constant.t * implicits_flags
   | ImplMutualInductive of MutInd.t * implicits_flags
-  | ImplInteractive of global_reference * implicits_flags *
+  | ImplInteractive of GlobRef.t * implicits_flags *
       implicit_interactive_request
 
 let implicits_table = Summary.ref Refmap.empty ~name:"implicits"
@@ -626,7 +626,7 @@ let classify_implicits (req,_ as obj) = match req with
 
 type implicits_obj =
     implicit_discharge_request *
-      (global_reference * implicits_list list) list
+      (GlobRef.t * implicits_list list) list
 
 let inImplicits : implicits_obj -> obj =
   declare_object {(default_object "IMPLICITS") with

interp/impargs.mli

@@ -10,7 +10,6 @@
 
 open Names
 open EConstr
-open Globnames
 open Environ
 
 (** {6 Implicit Arguments } *)
@@ -103,23 +102,23 @@ val declare_var_implicits : variable -> unit
 val declare_constant_implicits : Constant.t -> unit
 val declare_mib_implicits : MutInd.t -> unit
 
-val declare_implicits : bool -> global_reference -> unit
+val declare_implicits : bool -> GlobRef.t -> unit
 
 (** [declare_manual_implicits local ref enriching l]
    Manual declaration of which arguments are expected implicit.
    If not set, we decide if it should enrich by automatically inferd
    implicits depending on the current state.
    Unsets implicits if [l] is empty. *)
 
-val declare_manual_implicits : bool -> global_reference -> ?enriching:bool ->
+val declare_manual_implicits : bool -> GlobRef.t -> ?enriching:bool ->
   manual_implicits list -> unit
 
 (** If the list is empty, do nothing, otherwise declare the implicits. *)
 
-val maybe_declare_manual_implicits : bool -> global_reference -> ?enriching:bool ->
+val maybe_declare_manual_implicits : bool -> GlobRef.t -> ?enriching:bool ->
   manual_implicits -> unit
 
-val implicits_of_global : global_reference -> implicits_list list
+val implicits_of_global : GlobRef.t -> implicits_list list
 
 val extract_impargs_data :
   implicits_list list -> ((int * int) option * implicit_status list) list