From f3abbc55ef160d1a65d4467bfe9b25b30b965a46 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 4 Nov 2017 18:58:27 +0100 Subject: [api] Deprecate all legacy uses of Names in core. This will allow to merge back `Names` with `API.Names` --- library/coqlib.mli | 4 ++-- library/declaremods.ml | 24 ++++++++++++------------ library/declaremods.mli | 16 ++++++++-------- library/decls.mli | 4 ++-- library/global.mli | 44 ++++++++++++++++++++++---------------------- library/globnames.ml | 28 ++++++++++++++-------------- library/globnames.mli | 18 +++++++++--------- library/heads.ml | 4 ++-- library/lib.ml | 16 ++++++++-------- library/lib.mli | 26 +++++++++++++------------- library/libnames.ml | 8 ++++---- library/libnames.mli | 4 ++-- library/nametab.mli | 18 +++++++++--------- 13 files changed, 107 insertions(+), 107 deletions(-) (limited to 'library') diff --git a/library/coqlib.mli b/library/coqlib.mli index 1e3c37a9e..17c79d2e1 100644 --- a/library/coqlib.mli +++ b/library/coqlib.mli @@ -71,8 +71,8 @@ val jmeq_module_name : string list val datatypes_module_name : string list (** Identity *) -val id : constant -val type_of_id : constant +val id : Constant.t +val type_of_id : Constant.t (** Natural numbers *) val nat_path : full_path diff --git a/library/declaremods.ml b/library/declaremods.ml index 6d9295bde..cda40f49f 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -39,7 +39,7 @@ let inl2intopt = function type algebraic_objects = | Objs of Lib.lib_objects - | Ref of module_path * substitution + | Ref of ModPath.t * substitution type substitutive_objects = MBId.t list * algebraic_objects @@ -62,9 +62,9 @@ type substitutive_objects = MBId.t list * algebraic_objects module ModSubstObjs : sig - val set : module_path -> substitutive_objects -> unit - val get : module_path -> substitutive_objects - val set_missing_handler : (module_path -> substitutive_objects) -> unit + val set : ModPath.t -> substitutive_objects -> unit + val get : ModPath.t -> substitutive_objects + val set_missing_handler : (ModPath.t -> substitutive_objects) -> unit end = struct let table = @@ -126,8 +126,8 @@ type module_objects = object_prefix * Lib.lib_objects * Lib.lib_objects module ModObjs : sig - val set : module_path -> module_objects -> unit - val get : module_path -> module_objects (* may raise Not_found *) + val set : ModPath.t -> module_objects -> unit + val get : ModPath.t -> module_objects (* may raise Not_found *) val all : unit -> module_objects MPmap.t end = struct @@ -143,11 +143,11 @@ module ModObjs : (** {6 Name management} Auxiliary functions to transform full_path and kernel_name given - by Lib into module_path and DirPath.t needed for modules + by Lib into ModPath.t and DirPath.t needed for modules *) let mp_of_kn kn = - let mp,sec,l = repr_kn kn in + let mp,sec,l = KerName.repr kn in assert (DirPath.is_empty sec); MPdot (mp,l) @@ -336,8 +336,8 @@ let () = ModSubstObjs.set_missing_handler handle_missing_substobjs (** {6 From module expression to substitutive objects} *) -(** Turn a chain of [MSEapply] into the head module_path and the - list of module_path parameters (deepest param coming first). +(** Turn a chain of [MSEapply] into the head ModPath.t and the + list of ModPath.t parameters (deepest param coming first). The left part of a [MSEapply] must be either [MSEident] or another [MSEapply]. *) @@ -911,7 +911,7 @@ let subst_import (subst,(export,mp as obj)) = let mp' = subst_mp subst mp in if mp'==mp then obj else (export,mp') -let in_import : bool * module_path -> obj = +let in_import : bool * ModPath.t -> obj = declare_object {(default_object "IMPORT MODULE") with cache_function = cache_import; open_function = open_import; @@ -961,7 +961,7 @@ let debug_print_modtab _ = | l -> str "[." ++ int (List.length l) ++ str ".]" in let pr_modinfo mp (prefix,substobjs,keepobjs) s = - s ++ str (string_of_mp mp) ++ (spc ()) + s ++ str (ModPath.to_string mp) ++ (spc ()) ++ (pr_seg (Lib.segment_of_objects prefix (substobjs@keepobjs))) in let modules = MPmap.fold pr_modinfo (ModObjs.all ()) (mt ()) in diff --git a/library/declaremods.mli b/library/declaremods.mli index 9d750b616..90e86cd02 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -30,15 +30,15 @@ val declare_module : Id.t -> 'modast module_params -> ('modast * inline) module_signature -> - ('modast * inline) list -> module_path + ('modast * inline) list -> ModPath.t val start_module : 'modast module_interpretor -> bool option -> Id.t -> 'modast module_params -> - ('modast * inline) module_signature -> module_path + ('modast * inline) module_signature -> ModPath.t -val end_module : unit -> module_path +val end_module : unit -> ModPath.t @@ -53,15 +53,15 @@ val declare_modtype : 'modast module_params -> ('modast * inline) list -> ('modast * inline) list -> - module_path + ModPath.t val start_modtype : 'modast module_interpretor -> Id.t -> 'modast module_params -> - ('modast * inline) list -> module_path + ('modast * inline) list -> ModPath.t -val end_modtype : unit -> module_path +val end_modtype : unit -> ModPath.t (** {6 Libraries i.e. modules on disk } *) @@ -90,13 +90,13 @@ val append_end_library_hook : (unit -> unit) -> unit every object of the module. Raises [Not_found] when [mp] is unknown or when [mp] corresponds to a functor. *) -val really_import_module : module_path -> unit +val really_import_module : ModPath.t -> unit (** [import_module export mp] is a synchronous version of [really_import_module]. If [export] is [true], the module is also opened every time the module containing it is. *) -val import_module : bool -> module_path -> unit +val import_module : bool -> ModPath.t -> unit (** Include *) diff --git a/library/decls.mli b/library/decls.mli index 478f0bca0..524377257 100644 --- a/library/decls.mli +++ b/library/decls.mli @@ -30,8 +30,8 @@ val variable_exists : variable -> bool (** Registration and access to the table of constants *) -val add_constant_kind : constant -> logical_kind -> unit -val constant_kind : constant -> logical_kind +val add_constant_kind : Constant.t -> logical_kind -> unit +val constant_kind : Constant.t -> logical_kind (* Prepare global named context for proof session: remove proofs of opaque section definitions and remove vm-compiled code *) diff --git a/library/global.mli b/library/global.mli index 15bf58f82..1aff0a376 100644 --- a/library/global.mli +++ b/library/global.mli @@ -39,9 +39,9 @@ val export_private_constants : in_section:bool -> unit Entries.constant_entry * Safe_typing.exported_private_constant list val add_constant : - DirPath.t -> Id.t -> Safe_typing.global_declaration -> constant + DirPath.t -> Id.t -> Safe_typing.global_declaration -> Constant.t val add_mind : - DirPath.t -> Id.t -> Entries.mutual_inductive_entry -> mutual_inductive + DirPath.t -> Id.t -> Entries.mutual_inductive_entry -> MutInd.t (** Extra universe constraints *) val add_constraints : Univ.constraints -> unit @@ -53,23 +53,23 @@ val push_context_set : bool -> Univ.universe_context_set -> unit val add_module : Id.t -> Entries.module_entry -> Declarations.inline -> - module_path * Mod_subst.delta_resolver + ModPath.t * Mod_subst.delta_resolver val add_modtype : - Id.t -> Entries.module_type_entry -> Declarations.inline -> module_path + Id.t -> Entries.module_type_entry -> Declarations.inline -> ModPath.t val add_include : Entries.module_struct_entry -> bool -> Declarations.inline -> Mod_subst.delta_resolver (** Interactive modules and module types *) -val start_module : Id.t -> module_path -val start_modtype : Id.t -> module_path +val start_module : Id.t -> ModPath.t +val start_modtype : Id.t -> ModPath.t val end_module : Summary.frozen -> Id.t -> (Entries.module_struct_entry * Declarations.inline) option -> - module_path * MBId.t list * Mod_subst.delta_resolver + ModPath.t * MBId.t list * Mod_subst.delta_resolver -val end_modtype : Summary.frozen -> Id.t -> module_path * MBId.t list +val end_modtype : Summary.frozen -> Id.t -> ModPath.t * MBId.t list val add_module_parameter : MBId.t -> Entries.module_struct_entry -> Declarations.inline -> @@ -78,22 +78,22 @@ val add_module_parameter : (** {6 Queries in the global environment } *) val lookup_named : variable -> Context.Named.Declaration.t -val lookup_constant : constant -> Declarations.constant_body +val lookup_constant : Constant.t -> Declarations.constant_body val lookup_inductive : inductive -> Declarations.mutual_inductive_body * Declarations.one_inductive_body val lookup_pinductive : Constr.pinductive -> Declarations.mutual_inductive_body * Declarations.one_inductive_body -val lookup_mind : mutual_inductive -> Declarations.mutual_inductive_body -val lookup_module : module_path -> Declarations.module_body -val lookup_modtype : module_path -> Declarations.module_type_body +val lookup_mind : MutInd.t -> Declarations.mutual_inductive_body +val lookup_module : ModPath.t -> Declarations.module_body +val lookup_modtype : ModPath.t -> Declarations.module_type_body val exists_objlabel : Label.t -> bool -val constant_of_delta_kn : kernel_name -> constant -val mind_of_delta_kn : kernel_name -> mutual_inductive +val constant_of_delta_kn : KerName.t -> Constant.t +val mind_of_delta_kn : KerName.t -> MutInd.t val opaque_tables : unit -> Opaqueproof.opaquetab -val body_of_constant : constant -> (Term.constr * Univ.AUContext.t) option +val body_of_constant : Constant.t -> (Term.constr * Univ.AUContext.t) option (** Returns the body of the constant if it has any, and the polymorphic context it lives in. For monomorphic constant, the latter is empty, and for polymorphic constants, the term contains De Bruijn universe variables that @@ -111,12 +111,12 @@ val set_global_universe_names : universe_names -> unit (** {6 Compiled libraries } *) -val start_library : DirPath.t -> module_path +val start_library : DirPath.t -> ModPath.t val export : ?except:Future.UUIDSet.t -> DirPath.t -> - module_path * Safe_typing.compiled_library * Safe_typing.native_library + ModPath.t * Safe_typing.compiled_library * Safe_typing.native_library val import : Safe_typing.compiled_library -> Univ.universe_context_set -> Safe_typing.vodigest -> - module_path + ModPath.t (** {6 Misc } *) @@ -154,16 +154,16 @@ val universes_of_global : Globnames.global_reference -> Univ.abstract_universe_c val register : Retroknowledge.field -> Term.constr -> Term.constr -> unit -val register_inline : constant -> unit +val register_inline : Constant.t -> unit (** {6 Oracle } *) -val set_strategy : Names.constant Names.tableKey -> Conv_oracle.level -> unit +val set_strategy : Constant.t Names.tableKey -> Conv_oracle.level -> unit (* Modifies the global state, registering new universes *) -val current_dirpath : unit -> Names.dir_path +val current_dirpath : unit -> DirPath.t -val with_global : (Environ.env -> Names.dir_path -> 'a Univ.in_universe_context_set) -> 'a +val with_global : (Environ.env -> DirPath.t -> 'a Univ.in_universe_context_set) -> 'a val global_env_summary_name : string diff --git a/library/globnames.ml b/library/globnames.ml index 5c75994dd..9f652896c 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -15,7 +15,7 @@ open Libnames (*s Global reference is a kernel side type for all references together *) type global_reference = | VarRef of variable (** A reference to the section-context. *) - | ConstRef of constant (** A reference to the environment. *) + | 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. *) @@ -26,7 +26,7 @@ let isConstructRef = function ConstructRef _ -> true | _ -> false let eq_gr gr1 gr2 = gr1 == gr2 || match gr1,gr2 with - | ConstRef con1, ConstRef con2 -> eq_constant con1 con2 + | 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 @@ -67,9 +67,9 @@ let subst_global subst ref = match ref with if c'==c then ref,t else ConstructRef c', t let canonical_gr = function - | ConstRef con -> ConstRef(constant_of_kn(canonical_con con)) - | IndRef (kn,i) -> IndRef(mind_of_kn(canonical_mind kn),i) - | ConstructRef ((kn,i),j )-> ConstructRef((mind_of_kn(canonical_mind kn),i),j) + | ConstRef con -> ConstRef(Constant.make1 (Constant.canonical con)) + | IndRef (kn,i) -> IndRef(MutInd.make1(MutInd.canonical kn),i) + | ConstructRef ((kn,i),j )-> ConstructRef((MutInd.make1(MutInd.canonical kn),i),j) | VarRef id -> VarRef id let global_of_constr c = match kind_of_term c with @@ -81,7 +81,7 @@ let global_of_constr c = match kind_of_term c with let is_global c t = match c, kind_of_term t with - | ConstRef c, Const (c', _) -> eq_constant c c' + | ConstRef c, Const (c', _) -> Constant.equal c c' | IndRef i, Ind (i', _) -> eq_ind i i' | ConstructRef i, Construct (i', _) -> eq_constructor i i' | VarRef id, Var id' -> Id.equal id id' @@ -157,7 +157,7 @@ module Refset_env = Refmap_env.Set (* Extended global references *) -type syndef_name = kernel_name +type syndef_name = KerName.t type extended_global_reference = | TrueGlobal of global_reference @@ -180,7 +180,7 @@ module ExtRefOrdered = struct if x == y then 0 else match x, y with | TrueGlobal rx, TrueGlobal ry -> RefOrdered_env.compare rx ry - | SynDef knx, SynDef kny -> kn_ord knx kny + | SynDef knx, SynDef kny -> KerName.compare knx kny | TrueGlobal _, SynDef _ -> -1 | SynDef _, TrueGlobal _ -> 1 @@ -215,12 +215,12 @@ let decode_mind kn = id::(DirPath.repr dp) | MPdot(mp,l) -> (Label.to_id l)::(dir_of_mp mp) in - let mp,sec_dir,l = repr_mind kn in + let mp,sec_dir,l = MutInd.repr3 kn in check_empty_section sec_dir; (DirPath.make (dir_of_mp mp)),Label.to_id l let decode_con kn = - let mp,sec_dir,l = repr_con kn in + let mp,sec_dir,l = Constant.repr3 kn in check_empty_section sec_dir; match mp with | MPfile dir -> (dir,Label.to_id l) @@ -231,12 +231,12 @@ let decode_con kn = user and canonical kernel names must be equal. *) let pop_con con = - let (mp,dir,l) = repr_con con in - Names.make_con mp (pop_dirpath dir) l + let (mp,dir,l) = Constant.repr3 con in + Constant.make3 mp (pop_dirpath dir) l let pop_kn kn = - let (mp,dir,l) = repr_mind kn in - Names.make_mind mp (pop_dirpath dir) l + let (mp,dir,l) = MutInd.repr3 kn in + MutInd.make3 mp (pop_dirpath dir) l let pop_global_reference = function | ConstRef con -> ConstRef (pop_con con) diff --git a/library/globnames.mli b/library/globnames.mli index 0b5971b6e..361631bd3 100644 --- a/library/globnames.mli +++ b/library/globnames.mli @@ -14,7 +14,7 @@ open Mod_subst (** {6 Global reference is a kernel side type for all references together } *) type global_reference = | VarRef of variable (** A reference to the section-context. *) - | ConstRef of constant (** A reference to the environment. *) + | 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. *) @@ -27,7 +27,7 @@ val eq_gr : global_reference -> global_reference -> bool val canonical_gr : global_reference -> global_reference val destVarRef : global_reference -> variable -val destConstRef : global_reference -> constant +val destConstRef : global_reference -> Constant.t val destIndRef : global_reference -> inductive val destConstructRef : global_reference -> constructor @@ -72,7 +72,7 @@ module Refmap_env : Map.ExtS (** {6 Extended global references } *) -type syndef_name = kernel_name +type syndef_name = KerName.t type extended_global_reference = | TrueGlobal of global_reference @@ -91,13 +91,13 @@ type global_reference_or_constr = (** {6 Temporary function to brutally form kernel names from section paths } *) -val encode_mind : DirPath.t -> Id.t -> mutual_inductive -val decode_mind : mutual_inductive -> DirPath.t * Id.t -val encode_con : DirPath.t -> Id.t -> constant -val decode_con : constant -> DirPath.t * Id.t +val encode_mind : DirPath.t -> Id.t -> MutInd.t +val decode_mind : MutInd.t -> DirPath.t * Id.t +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 -> constant -val pop_kn : mutual_inductive-> mutual_inductive +val pop_con : Constant.t -> Constant.t +val pop_kn : MutInd.t-> MutInd.t val pop_global_reference : global_reference -> global_reference diff --git a/library/heads.ml b/library/heads.ml index c12fa9479..d2cfc0990 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -25,7 +25,7 @@ open Context.Named.Declaration the evaluation of [phi(0)] and the head of [h] is declared unknown). *) type rigid_head_kind = -| RigidParameter of constant (* a Const without body *) +| RigidParameter of Constant.t (* a Const without body *) | RigidVar of variable (* a Var without body *) | RigidType (* an inductive, a product or a sort *) @@ -156,7 +156,7 @@ let cache_head o = let subst_head_approximation subst = function | RigidHead (RigidParameter cst) as k -> let cst,c = subst_con_kn subst cst in - if isConst c && eq_constant (fst (destConst c)) cst then + if isConst c && Constant.equal (fst (destConst c)) cst then (* A change of the prefix of the constant *) k else diff --git a/library/lib.ml b/library/lib.ml index e95bb47f2..a6fa27be8 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -62,7 +62,7 @@ let classify_segment seg = let rec clean ((substl,keepl,anticipl) as acc) = function | (_,CompilingLibrary _) :: _ | [] -> acc | ((sp,kn),Leaf o) :: stk -> - let id = Names.Label.to_id (Names.label kn) in + let id = Names.Label.to_id (Names.KerName.label kn) in (match classify_object o with | Dispose -> clean acc stk | Keep o' -> @@ -93,12 +93,12 @@ let segment_of_objects prefix = sections, but on the contrary there are many constructions of section paths based on the library path. *) -let initial_prefix = default_library,(Names.initial_path,Names.DirPath.empty) +let initial_prefix = default_library,(Names.ModPath.initial,Names.DirPath.empty) type lib_state = { comp_name : Names.DirPath.t option; lib_stk : library_segment; - path_prefix : Names.DirPath.t * (Names.module_path * Names.DirPath.t); + path_prefix : Names.DirPath.t * (Names.ModPath.t * Names.DirPath.t); } let initial_lib_state = { @@ -137,7 +137,7 @@ let make_path_except_section id = let make_kn id = let mp,dir = current_prefix () in - Names.make_kn mp dir (Names.Label.of_id id) + Names.KerName.make mp dir (Names.Label.of_id id) let make_oname id = Libnames.make_oname !lib_state.path_prefix id @@ -226,7 +226,7 @@ let add_anonymous_entry node = add_entry (make_oname (anonymous_id ())) node let add_leaf id obj = - if Names.ModPath.equal (current_mp ()) Names.initial_path then + if Names.ModPath.equal (current_mp ()) Names.ModPath.initial then user_err Pp.(str "No session module started (use -top dir)"); let oname = make_oname id in cache_object (oname,obj); @@ -597,7 +597,7 @@ let init () = let mp_of_global = function |VarRef id -> current_mp () - |ConstRef cst -> Names.con_modpath cst + |ConstRef cst -> Names.Constant.modpath cst |IndRef ind -> Names.ind_modpath ind |ConstructRef constr -> Names.constr_modpath constr @@ -621,12 +621,12 @@ let library_part = function (* Discharging names *) let con_defined_in_sec kn = - let _,dir,_ = Names.repr_con kn in + let _,dir,_ = Names.Constant.repr3 kn in not (Names.DirPath.is_empty dir) && Names.DirPath.equal (pop_dirpath dir) (current_sections ()) let defined_in_sec kn = - let _,dir,_ = Names.repr_mind kn in + let _,dir,_ = Names.MutInd.repr3 kn in not (Names.DirPath.is_empty dir) && Names.DirPath.equal (pop_dirpath dir) (current_sections ()) diff --git a/library/lib.mli b/library/lib.mli index 3dcec1d53..f941fd6d4 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -81,8 +81,8 @@ val make_path : Names.Id.t -> Libnames.full_path val make_path_except_section : Names.Id.t -> Libnames.full_path (** Kernel-side names *) -val current_mp : unit -> Names.module_path -val make_kn : Names.Id.t -> Names.kernel_name +val current_mp : unit -> Names.ModPath.t +val make_kn : Names.Id.t -> Names.KerName.t (** Are we inside an opened section *) val sections_are_opened : unit -> bool @@ -103,11 +103,11 @@ val find_opening_node : Names.Id.t -> node (** {6 Modules and module types } *) val start_module : - export -> Names.module_ident -> Names.module_path -> + export -> Names.module_ident -> Names.ModPath.t -> Summary.frozen -> Libnames.object_prefix val start_modtype : - Names.module_ident -> Names.module_path -> + Names.module_ident -> Names.ModPath.t -> Summary.frozen -> Libnames.object_prefix val end_module : @@ -122,7 +122,7 @@ val end_modtype : (** {6 Compilation units } *) -val start_compilation : Names.DirPath.t -> Names.module_path -> unit +val start_compilation : Names.DirPath.t -> Names.ModPath.t -> unit val end_compilation_checks : Names.DirPath.t -> Libnames.object_name val end_compilation : Libnames.object_name-> Libnames.object_prefix * library_segment @@ -132,8 +132,8 @@ val end_compilation : val library_dp : unit -> Names.DirPath.t (** Extract the library part of a name even if in a section *) -val dp_of_mp : Names.module_path -> Names.DirPath.t -val split_modpath : Names.module_path -> Names.DirPath.t * Names.Id.t list +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 (** {6 Sections } *) @@ -158,8 +158,8 @@ type abstr_info = variable_context * Univ.universe_level_subst * Univ.AUContext. val instance_from_variable_context : variable_context -> Names.Id.t array val named_of_variable_context : variable_context -> Context.Named.t -val section_segment_of_constant : Names.constant -> abstr_info -val section_segment_of_mutual_inductive: Names.mutual_inductive -> abstr_info +val section_segment_of_constant : Names.Constant.t -> abstr_info +val section_segment_of_mutual_inductive: Names.MutInd.t -> abstr_info val variable_section_segment_of_reference : Globnames.global_reference -> variable_context val section_instance : Globnames.global_reference -> Univ.universe_instance * Names.Id.t array @@ -168,15 +168,15 @@ val is_in_section : Globnames.global_reference -> bool val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.universe_context_set -> unit val add_section_context : Univ.universe_context_set -> unit val add_section_constant : Decl_kinds.polymorphic -> - Names.constant -> Context.Named.t -> unit + Names.Constant.t -> Context.Named.t -> unit val add_section_kn : Decl_kinds.polymorphic -> - Names.mutual_inductive -> Context.Named.t -> unit + Names.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.mutual_inductive -> Names.mutual_inductive -val discharge_con : Names.constant -> Names.constant +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_abstract_universe_context : diff --git a/library/libnames.ml b/library/libnames.ml index 0453f15e8..efb1348ab 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -154,12 +154,12 @@ let qualid_of_dirpath dir = let (l,a) = split_dirpath dir in make_qualid l a -type object_name = full_path * kernel_name +type object_name = full_path * KerName.t -type object_prefix = DirPath.t * (module_path * DirPath.t) +type object_prefix = DirPath.t * (ModPath.t * DirPath.t) let make_oname (dirpath,(mp,dir)) id = - make_path dirpath id, make_kn mp dir (Label.of_id id) + make_path dirpath id, KerName.make mp dir (Label.of_id id) (* to this type are mapped DirPath.t's in the nametab *) type global_dir_reference = @@ -173,7 +173,7 @@ type global_dir_reference = let eq_op (d1, (mp1, p1)) (d2, (mp2, p2)) = DirPath.equal d1 d2 && DirPath.equal p1 p2 && - mp_eq mp1 mp2 + ModPath.equal mp1 mp2 let eq_global_dir_reference r1 r2 = match r1, r2 with | DirOpenModule op1, DirOpenModule op2 -> eq_op op1 op2 diff --git a/library/libnames.mli b/library/libnames.mli index 1b351290a..ab2585334 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -91,9 +91,9 @@ val qualid_of_ident : Id.t -> qualid can be substituted and a "syntactic" [full_path] which can be printed *) -type object_name = full_path * kernel_name +type object_name = full_path * KerName.t -type object_prefix = DirPath.t * (module_path * DirPath.t) +type object_prefix = DirPath.t * (ModPath.t * DirPath.t) val eq_op : object_prefix -> object_prefix -> bool diff --git a/library/nametab.mli b/library/nametab.mli index 3a380637c..c02447a7c 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -74,7 +74,7 @@ val error_global_not_found : ?loc:Loc.t -> qualid -> 'a type visibility = Until of int | Exactly of int val push : visibility -> full_path -> global_reference -> unit -val push_modtype : visibility -> full_path -> module_path -> 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 @@ -85,11 +85,11 @@ val push_syndef : visibility -> full_path -> syndef_name -> unit val locate : qualid -> global_reference val locate_extended : qualid -> extended_global_reference -val locate_constant : qualid -> constant +val locate_constant : qualid -> Constant.t val locate_syndef : qualid -> syndef_name -val locate_modtype : qualid -> module_path +val locate_modtype : qualid -> ModPath.t val locate_dir : qualid -> global_dir_reference -val locate_module : qualid -> module_path +val locate_module : qualid -> ModPath.t val locate_section : qualid -> DirPath.t (** These functions globalize user-level references into global @@ -105,7 +105,7 @@ val global_inductive : reference -> inductive val locate_all : qualid -> global_reference 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 -> module_path list +val locate_extended_all_modtype : qualid -> ModPath.t list (** Mapping a full path to a global reference *) @@ -135,8 +135,8 @@ val full_name_module : qualid -> DirPath.t val path_of_syndef : syndef_name -> full_path val path_of_global : global_reference -> full_path -val dirpath_of_module : module_path -> DirPath.t -val path_of_modtype : module_path -> full_path +val dirpath_of_module : ModPath.t -> DirPath.t +val path_of_modtype : ModPath.t -> full_path (** Returns in particular the dirpath or the basename of the full path associated to global reference *) @@ -156,8 +156,8 @@ val pr_global_env : Id.Set.t -> global_reference -> Pp.t val shortest_qualid_of_global : Id.Set.t -> global_reference -> qualid val shortest_qualid_of_syndef : Id.Set.t -> syndef_name -> qualid -val shortest_qualid_of_modtype : module_path -> qualid -val shortest_qualid_of_module : module_path -> qualid +val shortest_qualid_of_modtype : ModPath.t -> qualid +val shortest_qualid_of_module : ModPath.t -> qualid (** Deprecated synonyms *) -- cgit v1.2.3