From afceace455a4b37ced7e29175ca3424996195f7b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 14 Nov 2017 22:36:47 +0100 Subject: [api] Rename `global_reference` to `GlobRef.t` to follow kernel style. In #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. --- library/coqlib.ml | 34 +++++++------- library/coqlib.mli | 123 +++++++++++++++++++++++++------------------------- library/global.mli | 12 ++--- library/globnames.ml | 13 ++---- library/globnames.mli | 55 +++++++++++----------- library/keys.ml | 7 +-- library/keys.mli | 4 +- library/lib.mli | 72 ++++++++++++++--------------- library/nametab.mli | 22 ++++----- 9 files changed, 168 insertions(+), 174 deletions(-) (limited to 'library') diff --git a/library/coqlib.ml b/library/coqlib.ml index 3f01c617c..408e25919 100644 --- a/library/coqlib.ml +++ b/library/coqlib.ml @@ -171,16 +171,16 @@ let jmeq_kn = make_ind jmeq_module "JMeq" let glob_jmeq = IndRef (jmeq_kn,0) type coq_sigma_data = { - proj1 : global_reference; - proj2 : global_reference; - elim : global_reference; - intro : global_reference; - typ : global_reference } + proj1 : GlobRef.t; + proj2 : GlobRef.t; + elim : GlobRef.t; + intro : GlobRef.t; + typ : GlobRef.t } type coq_bool_data = { - andb : global_reference; - andb_prop : global_reference; - andb_true_intro : global_reference} + andb : GlobRef.t; + andb_prop : GlobRef.t; + andb_true_intro : GlobRef.t} let build_bool_type () = { andb = init_reference ["Datatypes"] "andb"; @@ -213,18 +213,18 @@ let build_prod () = (* Equalities *) type coq_eq_data = { - eq : global_reference; - ind : global_reference; - refl : global_reference; - sym : global_reference; - trans: global_reference; - congr: global_reference } + eq : GlobRef.t; + ind : GlobRef.t; + refl : GlobRef.t; + sym : GlobRef.t; + trans: GlobRef.t; + congr: GlobRef.t } (* Data needed for discriminate and injection *) type coq_inversion_data = { - inv_eq : global_reference; (* : forall params, t -> Prop *) - inv_ind : global_reference; (* : forall params P y, eq params y -> P y *) - inv_congr: global_reference (* : forall params B (f:t->B) y, eq params y -> f c=f y *) + inv_eq : GlobRef.t; (* : forall params, t -> Prop *) + inv_ind : GlobRef.t; (* : forall params P y, eq params y -> P y *) + inv_congr: GlobRef.t (* : forall params B (f:t->B) y, eq params y -> f c=f y *) } let lazy_init_reference dir id = lazy (init_reference dir id) diff --git a/library/coqlib.mli b/library/coqlib.mli index 8077c47c7..b4bd1b0e0 100644 --- a/library/coqlib.mli +++ b/library/coqlib.mli @@ -8,10 +8,9 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open Util open Names open Libnames -open Globnames -open Util (** This module collects the global references, constructions and patterns of the standard library used in ocaml files *) @@ -44,14 +43,14 @@ open Util type message = string -val find_reference : message -> string list -> string -> global_reference -val coq_reference : message -> string list -> string -> global_reference +val find_reference : message -> string list -> string -> GlobRef.t +val coq_reference : message -> string list -> string -> GlobRef.t (** For tactics/commands requiring vernacular libraries *) val check_required_library : string list -> unit (** Search in several modules (not prefixed by "Coq") *) -val gen_reference_in_modules : string->string list list-> string -> global_reference +val gen_reference_in_modules : string->string list list-> string -> GlobRef.t val arith_modules : string list list val zarith_base_modules : string list list @@ -78,24 +77,24 @@ val type_of_id : Constant.t (** Natural numbers *) val nat_path : full_path -val glob_nat : global_reference +val glob_nat : GlobRef.t val path_of_O : constructor val path_of_S : constructor -val glob_O : global_reference -val glob_S : global_reference +val glob_O : GlobRef.t +val glob_S : GlobRef.t (** Booleans *) -val glob_bool : global_reference +val glob_bool : GlobRef.t val path_of_true : constructor val path_of_false : constructor -val glob_true : global_reference -val glob_false : global_reference +val glob_true : GlobRef.t +val glob_false : GlobRef.t (** Equality *) -val glob_eq : global_reference -val glob_identity : global_reference -val glob_jmeq : global_reference +val glob_eq : GlobRef.t +val glob_identity : GlobRef.t +val glob_jmeq : GlobRef.t (** {6 ... } *) (** Constructions and patterns related to Coq initial state are unknown @@ -106,18 +105,18 @@ val glob_jmeq : global_reference at runtime. *) type coq_bool_data = { - andb : global_reference; - andb_prop : global_reference; - andb_true_intro : global_reference} + andb : GlobRef.t; + andb_prop : GlobRef.t; + andb_true_intro : GlobRef.t} val build_bool_type : coq_bool_data delayed (** {6 For Equality tactics } *) type coq_sigma_data = { - proj1 : global_reference; - proj2 : global_reference; - elim : global_reference; - intro : global_reference; - typ : global_reference } + proj1 : GlobRef.t; + proj2 : GlobRef.t; + elim : GlobRef.t; + intro : GlobRef.t; + typ : GlobRef.t } val build_sigma_set : coq_sigma_data delayed val build_sigma_type : coq_sigma_data delayed @@ -132,30 +131,30 @@ val build_sigma : coq_sigma_data delayed val build_prod : coq_sigma_data delayed type coq_eq_data = { - eq : global_reference; - ind : global_reference; - refl : global_reference; - sym : global_reference; - trans: global_reference; - congr: global_reference } + eq : GlobRef.t; + ind : GlobRef.t; + refl : GlobRef.t; + sym : GlobRef.t; + trans: GlobRef.t; + congr: GlobRef.t } val build_coq_eq_data : coq_eq_data delayed val build_coq_identity_data : coq_eq_data delayed val build_coq_jmeq_data : coq_eq_data delayed -val build_coq_eq : global_reference delayed (** = [(build_coq_eq_data()).eq] *) -val build_coq_eq_refl : global_reference delayed (** = [(build_coq_eq_data()).refl] *) -val build_coq_eq_sym : global_reference delayed (** = [(build_coq_eq_data()).sym] *) -val build_coq_f_equal2 : global_reference delayed +val build_coq_eq : GlobRef.t delayed (** = [(build_coq_eq_data()).eq] *) +val build_coq_eq_refl : GlobRef.t delayed (** = [(build_coq_eq_data()).refl] *) +val build_coq_eq_sym : GlobRef.t delayed (** = [(build_coq_eq_data()).sym] *) +val build_coq_f_equal2 : GlobRef.t delayed (** Data needed for discriminate and injection *) type coq_inversion_data = { - inv_eq : global_reference; (** : forall params, args -> Prop *) - inv_ind : global_reference; (** : forall params P (H : P params) args, eq params args + inv_eq : GlobRef.t; (** : forall params, args -> Prop *) + inv_ind : GlobRef.t; (** : forall params P (H : P params) args, eq params args -> P args *) - inv_congr: global_reference (** : forall params B (f:t->B) args, eq params args -> + inv_congr: GlobRef.t (** : forall params B (f:t->B) args, eq params args -> f params = f args *) } @@ -165,45 +164,45 @@ val build_coq_inversion_jmeq_data : coq_inversion_data delayed val build_coq_inversion_eq_true_data : coq_inversion_data delayed (** Specif *) -val build_coq_sumbool : global_reference delayed +val build_coq_sumbool : GlobRef.t delayed (** {6 ... } *) (** Connectives The False proposition *) -val build_coq_False : global_reference delayed +val build_coq_False : GlobRef.t delayed (** The True proposition and its unique proof *) -val build_coq_True : global_reference delayed -val build_coq_I : global_reference delayed +val build_coq_True : GlobRef.t delayed +val build_coq_I : GlobRef.t delayed (** Negation *) -val build_coq_not : global_reference delayed +val build_coq_not : GlobRef.t delayed (** Conjunction *) -val build_coq_and : global_reference delayed -val build_coq_conj : global_reference delayed -val build_coq_iff : global_reference delayed +val build_coq_and : GlobRef.t delayed +val build_coq_conj : GlobRef.t delayed +val build_coq_iff : GlobRef.t delayed -val build_coq_iff_left_proj : global_reference delayed -val build_coq_iff_right_proj : global_reference delayed +val build_coq_iff_left_proj : GlobRef.t delayed +val build_coq_iff_right_proj : GlobRef.t delayed (** Disjunction *) -val build_coq_or : global_reference delayed +val build_coq_or : GlobRef.t delayed (** Existential quantifier *) -val build_coq_ex : global_reference delayed - -val coq_eq_ref : global_reference lazy_t -val coq_identity_ref : global_reference lazy_t -val coq_jmeq_ref : global_reference lazy_t -val coq_eq_true_ref : global_reference lazy_t -val coq_existS_ref : global_reference lazy_t -val coq_existT_ref : global_reference lazy_t -val coq_exist_ref : global_reference lazy_t -val coq_not_ref : global_reference lazy_t -val coq_False_ref : global_reference lazy_t -val coq_sumbool_ref : global_reference lazy_t -val coq_sig_ref : global_reference lazy_t - -val coq_or_ref : global_reference lazy_t -val coq_iff_ref : global_reference lazy_t +val build_coq_ex : GlobRef.t delayed + +val coq_eq_ref : GlobRef.t lazy_t +val coq_identity_ref : GlobRef.t lazy_t +val coq_jmeq_ref : GlobRef.t lazy_t +val coq_eq_true_ref : GlobRef.t lazy_t +val coq_existS_ref : GlobRef.t lazy_t +val coq_existT_ref : GlobRef.t lazy_t +val coq_exist_ref : GlobRef.t lazy_t +val coq_not_ref : GlobRef.t lazy_t +val coq_False_ref : GlobRef.t lazy_t +val coq_sumbool_ref : GlobRef.t lazy_t +val coq_sig_ref : GlobRef.t lazy_t + +val coq_or_ref : GlobRef.t lazy_t +val coq_iff_ref : GlobRef.t lazy_t diff --git a/library/global.mli b/library/global.mli index 015f4d582..906d246ee 100644 --- a/library/global.mli +++ b/library/global.mli @@ -123,26 +123,26 @@ val env_of_context : Environ.named_context_val -> Environ.env val join_safe_environment : ?except:Future.UUIDSet.t -> unit -> unit val is_joined_environment : unit -> bool -val is_polymorphic : Globnames.global_reference -> bool -val is_template_polymorphic : Globnames.global_reference -> bool -val is_type_in_type : Globnames.global_reference -> bool +val is_polymorphic : GlobRef.t -> bool +val is_template_polymorphic : GlobRef.t -> bool +val is_type_in_type : GlobRef.t -> bool val constr_of_global_in_context : Environ.env -> - Globnames.global_reference -> Constr.types * Univ.AUContext.t + GlobRef.t -> Constr.types * Univ.AUContext.t (** Returns the type of the constant in its local universe context. The type should not be used without pushing it's universe context in the environmnent of usage. For non-universe-polymorphic constants, it does not matter. *) val type_of_global_in_context : Environ.env -> - Globnames.global_reference -> Constr.types * Univ.AUContext.t + GlobRef.t -> Constr.types * Univ.AUContext.t (** Returns the type of the constant in its local universe context. The type should not be used without pushing it's universe context in the environmnent of usage. For non-universe-polymorphic constants, it does not matter. *) (** Returns the universe context of the global reference (whatever its polymorphic status is). *) -val universes_of_global : Globnames.global_reference -> Univ.AUContext.t +val universes_of_global : GlobRef.t -> Univ.AUContext.t (** {6 Retroknowledge } *) diff --git a/library/globnames.ml b/library/globnames.ml index 2fa3adba2..6b78d12ba 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -15,7 +15,7 @@ open Mod_subst open Libnames (*s Global reference is a kernel side type for all references together *) -type global_reference = Names.global_reference = +type global_reference = GlobRef.t = | VarRef of variable (** A reference to the section-context. *) | ConstRef of Constant.t (** A reference to the environment. *) | IndRef of inductive (** A reference to an inductive type. *) @@ -26,14 +26,6 @@ let isConstRef = function ConstRef _ -> true | _ -> false let isIndRef = function IndRef _ -> true | _ -> false let isConstructRef = function ConstructRef _ -> true | _ -> false -let eq_gr gr1 gr2 = - gr1 == gr2 || match gr1,gr2 with - | ConstRef con1, ConstRef con2 -> Constant.equal con1 con2 - | IndRef kn1, IndRef kn2 -> eq_ind kn1 kn2 - | ConstructRef kn1, ConstructRef kn2 -> eq_constructor kn1 kn2 - | VarRef v1, VarRef v2 -> Id.equal v1 v2 - | (ConstRef _ | IndRef _ | ConstructRef _ | VarRef _), _ -> false - let destVarRef = function VarRef ind -> ind | _ -> failwith "destVarRef" let destConstRef = function ConstRef ind -> ind | _ -> failwith "destConstRef" let destIndRef = function IndRef ind -> ind | _ -> failwith "destIndRef" @@ -245,3 +237,6 @@ let pop_global_reference = function | IndRef (kn,i) -> IndRef (pop_kn kn,i) | ConstructRef ((kn,i),j) -> ConstructRef ((pop_kn kn,i),j) | VarRef id -> anomaly (Pp.str "VarRef not poppable.") + +(* Deprecated *) +let eq_gr = GlobRef.equal diff --git a/library/globnames.mli b/library/globnames.mli index f2b88b870..2fe35ebcc 100644 --- a/library/globnames.mli +++ b/library/globnames.mli @@ -14,71 +14,73 @@ open Constr open Mod_subst (** {6 Global reference is a kernel side type for all references together } *) -type global_reference = Names.global_reference = +type global_reference = GlobRef.t = | VarRef of variable (** A reference to the section-context. *) | ConstRef of Constant.t (** A reference to the environment. *) | IndRef of inductive (** A reference to an inductive type. *) | ConstructRef of constructor (** A reference to a constructor of an inductive type. *) +[@@ocaml.deprecated "Use Names.GlobRef.t"] -val isVarRef : global_reference -> bool -val isConstRef : global_reference -> bool -val isIndRef : global_reference -> bool -val isConstructRef : global_reference -> bool +val isVarRef : GlobRef.t -> bool +val isConstRef : GlobRef.t -> bool +val isIndRef : GlobRef.t -> bool +val isConstructRef : GlobRef.t -> bool -val eq_gr : global_reference -> global_reference -> bool -val canonical_gr : global_reference -> global_reference +val eq_gr : GlobRef.t -> GlobRef.t -> bool +[@@ocaml.deprecated "Use Names.GlobRef.equal"] +val canonical_gr : GlobRef.t -> GlobRef.t -val destVarRef : global_reference -> variable -val destConstRef : global_reference -> Constant.t -val destIndRef : global_reference -> inductive -val destConstructRef : global_reference -> constructor +val destVarRef : GlobRef.t -> variable +val destConstRef : GlobRef.t -> Constant.t +val destIndRef : GlobRef.t -> inductive +val destConstructRef : GlobRef.t -> constructor -val is_global : global_reference -> constr -> bool +val is_global : GlobRef.t -> constr -> bool val subst_constructor : substitution -> constructor -> constructor * constr -val subst_global : substitution -> global_reference -> global_reference * constr -val subst_global_reference : substitution -> global_reference -> global_reference +val subst_global : substitution -> GlobRef.t -> GlobRef.t * constr +val subst_global_reference : substitution -> GlobRef.t -> GlobRef.t (** This constr is not safe to be typechecked, universe polymorphism is not handled here: just use for printing *) -val printable_constr_of_global : global_reference -> constr +val printable_constr_of_global : GlobRef.t -> constr (** Turn a construction denoting a global reference into a global reference; raise [Not_found] if not a global reference *) -val global_of_constr : constr -> global_reference +val global_of_constr : constr -> GlobRef.t (** Obsolete synonyms for constr_of_global and global_of_constr *) -val reference_of_constr : constr -> global_reference +val reference_of_constr : constr -> GlobRef.t [@@ocaml.deprecated "Alias of Globnames.global_of_constr"] module RefOrdered : sig - type t = global_reference + type t = GlobRef.t val compare : t -> t -> int val equal : t -> t -> bool val hash : t -> int end module RefOrdered_env : sig - type t = global_reference + type t = GlobRef.t val compare : t -> t -> int val equal : t -> t -> bool val hash : t -> int end -module Refset : CSig.SetS with type elt = global_reference +module Refset : CSig.SetS with type elt = GlobRef.t module Refmap : Map.ExtS - with type key = global_reference and module Set := Refset + with type key = GlobRef.t and module Set := Refset -module Refset_env : CSig.SetS with type elt = global_reference +module Refset_env : CSig.SetS with type elt = GlobRef.t module Refmap_env : Map.ExtS - with type key = global_reference and module Set := Refset_env + with type key = GlobRef.t and module Set := Refset_env (** {6 Extended global references } *) type syndef_name = KerName.t type extended_global_reference = - | TrueGlobal of global_reference + | TrueGlobal of GlobRef.t | SynDef of syndef_name module ExtRefOrdered : sig @@ -89,7 +91,7 @@ module ExtRefOrdered : sig end type global_reference_or_constr = - | IsGlobal of global_reference + | IsGlobal of GlobRef.t | IsConstr of constr (** {6 Temporary function to brutally form kernel names from section paths } *) @@ -100,7 +102,6 @@ val encode_con : DirPath.t -> Id.t -> Constant.t val decode_con : Constant.t -> DirPath.t * Id.t (** {6 Popping one level of section in global names } *) - val pop_con : Constant.t -> Constant.t val pop_kn : MutInd.t-> MutInd.t -val pop_global_reference : global_reference -> global_reference +val pop_global_reference : GlobRef.t -> GlobRef.t diff --git a/library/keys.ml b/library/keys.ml index 34a6adabe..89363455d 100644 --- a/library/keys.ml +++ b/library/keys.ml @@ -10,12 +10,13 @@ (** Keys for unification and indexing *) -open Globnames +open Names open Term +open Globnames open Libobject type key = - | KGlob of global_reference + | KGlob of GlobRef.t | KLam | KLet | KProd @@ -126,7 +127,7 @@ let constr_key kind c = | Construct (c,u) -> KGlob (ConstructRef c) | Var id -> KGlob (VarRef id) | App (f, _) -> aux f - | Proj (p, _) -> KGlob (ConstRef (Names.Projection.constant p)) + | Proj (p, _) -> KGlob (ConstRef (Projection.constant p)) | Cast (p, _, _) -> aux p | Lambda _ -> KLam | Prod _ -> KProd diff --git a/library/keys.mli b/library/keys.mli index 1fb9a3de0..198383650 100644 --- a/library/keys.mli +++ b/library/keys.mli @@ -8,8 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Globnames - type key val declare_equiv_keys : key -> key -> unit @@ -21,5 +19,5 @@ val equiv_keys : key -> key -> bool val constr_key : ('a -> ('a, 't, 'u, 'i) Constr.kind_of_term) -> 'a -> key option (** Compute the head key of a term. *) -val pr_keys : (global_reference -> Pp.t) -> Pp.t +val pr_keys : (Names.GlobRef.t -> Pp.t) -> Pp.t (** Pretty-print the mapping *) diff --git a/library/lib.mli b/library/lib.mli index 26f1718cc..1d77212e9 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) - +open Names (** Lib: record of operations, backtrack, low-level sections *) (** This module provides a general mechanism to keep a trace of all operations @@ -28,7 +28,7 @@ type node = and library_segment = (Libnames.object_name * node) list -type lib_objects = (Names.Id.t * Libobject.obj) list +type lib_objects = (Id.t * Libobject.obj) list (** {6 Object iteration functions. } *) @@ -54,13 +54,13 @@ val segment_of_objects : (** Adding operations (which call the [cache] method, and getting the current list of operations (most recent ones coming first). *) -val add_leaf : Names.Id.t -> Libobject.obj -> Libnames.object_name +val add_leaf : Id.t -> Libobject.obj -> Libnames.object_name val add_anonymous_leaf : ?cache_first:bool -> Libobject.obj -> unit val pull_to_head : Libnames.object_name -> unit (** this operation adds all objects with the same name and calls [load_object] for each of them *) -val add_leaves : Names.Id.t -> Libobject.obj list -> Libnames.object_name +val add_leaves : Id.t -> Libobject.obj list -> Libnames.object_name (** {6 ... } *) @@ -76,15 +76,15 @@ val contents_after : Libnames.object_name -> library_segment (** {6 Functions relative to current path } *) (** User-side names *) -val cwd : unit -> Names.DirPath.t -val cwd_except_section : unit -> Names.DirPath.t -val current_dirpath : bool -> Names.DirPath.t (* false = except sections *) -val make_path : Names.Id.t -> Libnames.full_path -val make_path_except_section : Names.Id.t -> Libnames.full_path +val cwd : unit -> DirPath.t +val cwd_except_section : unit -> DirPath.t +val current_dirpath : bool -> DirPath.t (* false = except sections *) +val make_path : Id.t -> Libnames.full_path +val make_path_except_section : Id.t -> Libnames.full_path (** Kernel-side names *) -val current_mp : unit -> Names.ModPath.t -val make_kn : Names.Id.t -> Names.KerName.t +val current_mp : unit -> ModPath.t +val make_kn : Id.t -> KerName.t (** Are we inside an opened section *) val sections_are_opened : unit -> bool @@ -97,19 +97,19 @@ val is_modtype : unit -> bool if the latest module started is a module type. *) val is_modtype_strict : unit -> bool val is_module : unit -> bool -val current_mod_id : unit -> Names.module_ident +val current_mod_id : unit -> module_ident (** Returns the opening node of a given name *) -val find_opening_node : Names.Id.t -> node +val find_opening_node : Id.t -> node (** {6 Modules and module types } *) val start_module : - export -> Names.module_ident -> Names.ModPath.t -> + export -> module_ident -> ModPath.t -> Summary.frozen -> Libnames.object_prefix val start_modtype : - Names.module_ident -> Names.ModPath.t -> + module_ident -> ModPath.t -> Summary.frozen -> Libnames.object_prefix val end_module : @@ -124,23 +124,23 @@ val end_modtype : (** {6 Compilation units } *) -val start_compilation : Names.DirPath.t -> Names.ModPath.t -> unit -val end_compilation_checks : Names.DirPath.t -> Libnames.object_name +val start_compilation : DirPath.t -> ModPath.t -> unit +val end_compilation_checks : DirPath.t -> Libnames.object_name val end_compilation : Libnames.object_name-> Libnames.object_prefix * library_segment (** The function [library_dp] returns the [DirPath.t] of the current compiling library (or [default_library]) *) -val library_dp : unit -> Names.DirPath.t +val library_dp : unit -> DirPath.t (** Extract the library part of a name even if in a section *) -val dp_of_mp : Names.ModPath.t -> Names.DirPath.t -val split_modpath : Names.ModPath.t -> Names.DirPath.t * Names.Id.t list -val library_part : Globnames.global_reference -> Names.DirPath.t +val dp_of_mp : ModPath.t -> DirPath.t +val split_modpath : ModPath.t -> DirPath.t * Id.t list +val library_part : GlobRef.t -> DirPath.t (** {6 Sections } *) -val open_section : Names.Id.t -> unit +val open_section : Id.t -> unit val close_section : unit -> unit (** {6 We can get and set the state of the operations (used in [States]). } *) @@ -164,31 +164,31 @@ type abstr_info = private { (** Universe quantification, same length as the substitution *) } -val instance_from_variable_context : variable_context -> Names.Id.t array +val instance_from_variable_context : variable_context -> Id.t array val named_of_variable_context : variable_context -> Context.Named.t -val section_segment_of_constant : Names.Constant.t -> abstr_info -val section_segment_of_mutual_inductive: Names.MutInd.t -> abstr_info -val section_segment_of_reference : Globnames.global_reference -> abstr_info +val section_segment_of_constant : Constant.t -> abstr_info +val section_segment_of_mutual_inductive: MutInd.t -> abstr_info +val section_segment_of_reference : GlobRef.t -> abstr_info -val variable_section_segment_of_reference : Globnames.global_reference -> variable_context +val variable_section_segment_of_reference : GlobRef.t -> variable_context -val section_instance : Globnames.global_reference -> Univ.Instance.t * Names.Id.t array -val is_in_section : Globnames.global_reference -> bool +val section_instance : GlobRef.t -> Univ.Instance.t * Id.t array +val is_in_section : GlobRef.t -> bool -val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.ContextSet.t -> unit +val add_section_variable : Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.ContextSet.t -> unit val add_section_context : Univ.ContextSet.t -> unit val add_section_constant : Decl_kinds.polymorphic -> - Names.Constant.t -> Context.Named.t -> unit + Constant.t -> Context.Named.t -> unit val add_section_kn : Decl_kinds.polymorphic -> - Names.MutInd.t -> Context.Named.t -> unit + MutInd.t -> Context.Named.t -> unit val replacement_context : unit -> Opaqueproof.work_list (** {6 Discharge: decrease the section level if in the current section } *) -val discharge_kn : Names.MutInd.t -> Names.MutInd.t -val discharge_con : Names.Constant.t -> Names.Constant.t -val discharge_global : Globnames.global_reference -> Globnames.global_reference -val discharge_inductive : Names.inductive -> Names.inductive +val discharge_kn : MutInd.t -> MutInd.t +val discharge_con : Constant.t -> Constant.t +val discharge_global : GlobRef.t -> GlobRef.t +val discharge_inductive : inductive -> inductive val discharge_abstract_universe_context : abstr_info -> Univ.AUContext.t -> Univ.universe_level_subst * Univ.AUContext.t diff --git a/library/nametab.mli b/library/nametab.mli index cd28518ab..2ec73a986 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -75,7 +75,7 @@ val error_global_not_found : qualid CAst.t -> 'a type visibility = Until of int | Exactly of int -val push : visibility -> full_path -> global_reference -> unit +val push : visibility -> full_path -> GlobRef.t -> unit val push_modtype : visibility -> full_path -> ModPath.t -> unit val push_dir : visibility -> DirPath.t -> global_dir_reference -> unit val push_syndef : visibility -> full_path -> syndef_name -> unit @@ -91,7 +91,7 @@ val push_universe : visibility -> full_path -> universe_id -> unit (** These functions globalize a (partially) qualified name or fail with [Not_found] *) -val locate : qualid -> global_reference +val locate : qualid -> GlobRef.t val locate_extended : qualid -> extended_global_reference val locate_constant : qualid -> Constant.t val locate_syndef : qualid -> syndef_name @@ -105,20 +105,20 @@ val locate_universe : qualid -> universe_id references, like [locate] and co, but raise a nice error message in case of failure *) -val global : reference -> global_reference +val global : reference -> GlobRef.t val global_inductive : reference -> inductive (** These functions locate all global references with a given suffix; if [qualid] is valid as such, it comes first in the list *) -val locate_all : qualid -> global_reference list +val locate_all : qualid -> GlobRef.t list val locate_extended_all : qualid -> extended_global_reference list val locate_extended_all_dir : qualid -> global_dir_reference list val locate_extended_all_modtype : qualid -> ModPath.t list (** Mapping a full path to a global reference *) -val global_of_path : full_path -> global_reference +val global_of_path : full_path -> GlobRef.t val extended_global_of_path : full_path -> extended_global_reference (** {6 These functions tell if the given absolute name is already taken } *) @@ -144,7 +144,7 @@ val full_name_module : qualid -> DirPath.t definition, and the (full) dirpath associated to a module path *) val path_of_syndef : syndef_name -> full_path -val path_of_global : global_reference -> full_path +val path_of_global : GlobRef.t -> full_path val dirpath_of_module : ModPath.t -> DirPath.t val path_of_modtype : ModPath.t -> full_path @@ -155,12 +155,12 @@ val path_of_universe : universe_id -> full_path (** Returns in particular the dirpath or the basename of the full path associated to global reference *) -val dirpath_of_global : global_reference -> DirPath.t -val basename_of_global : global_reference -> Id.t +val dirpath_of_global : GlobRef.t -> DirPath.t +val basename_of_global : GlobRef.t -> Id.t (** Printing of global references using names as short as possible. @raise Not_found when the reference is not in the global tables. *) -val pr_global_env : Id.Set.t -> global_reference -> Pp.t +val pr_global_env : Id.Set.t -> GlobRef.t -> Pp.t (** The [shortest_qualid] functions given an object with [user_name] @@ -168,7 +168,7 @@ val pr_global_env : Id.Set.t -> global_reference -> Pp.t Coq.A.B.x that denotes the same object. @raise Not_found for unknown objects. *) -val shortest_qualid_of_global : Id.Set.t -> global_reference -> qualid +val shortest_qualid_of_global : Id.Set.t -> GlobRef.t -> qualid val shortest_qualid_of_syndef : Id.Set.t -> syndef_name -> qualid val shortest_qualid_of_modtype : ModPath.t -> qualid val shortest_qualid_of_module : ModPath.t -> qualid @@ -177,7 +177,7 @@ val shortest_qualid_of_universe : universe_id -> qualid (** Deprecated synonyms *) val extended_locate : qualid -> extended_global_reference (*= locate_extended *) -val absolute_reference : full_path -> global_reference (** = global_of_path *) +val absolute_reference : full_path -> GlobRef.t (** = global_of_path *) (** {5 Generic name handling} *) -- cgit v1.2.3