diff options
| -rw-r--r-- | interp/declare.mli | 5 | ||||
| -rw-r--r-- | library/declaremods.mli | 2 | ||||
| -rw-r--r-- | library/lib.ml | 2 | ||||
| -rw-r--r-- | library/lib.mli | 18 | ||||
| -rw-r--r-- | library/libnames.ml | 6 | ||||
| -rw-r--r-- | library/libnames.mli | 8 | ||||
| -rw-r--r-- | library/libobject.ml | 6 | ||||
| -rw-r--r-- | library/libobject.mli | 7 | ||||
| -rw-r--r-- | printing/prettyp.mli | 4 |
9 files changed, 28 insertions, 30 deletions
diff --git a/interp/declare.mli b/interp/declare.mli index 02e73cd66c..468e056909 100644 --- a/interp/declare.mli +++ b/interp/declare.mli @@ -9,7 +9,6 @@ (************************************************************************) open Names -open Libnames open Constr open Entries open Decl_kinds @@ -29,7 +28,7 @@ type section_variable_entry = type variable_declaration = DirPath.t * section_variable_entry * logical_kind -val declare_variable : variable -> variable_declaration -> object_name +val declare_variable : variable -> variable_declaration -> Libobject.object_name (** Declaration of global constructions i.e. Definition/Theorem/Axiom/Parameter/... *) @@ -69,7 +68,7 @@ val set_declare_scheme : (** [declare_mind me] declares a block of inductive types with their constructors in the current section; it returns the path of the whole block and a boolean indicating if it is a primitive record. *) -val declare_mind : mutual_inductive_entry -> object_name * bool +val declare_mind : mutual_inductive_entry -> Libobject.object_name * bool (** Declaration messages *) diff --git a/library/declaremods.mli b/library/declaremods.mli index b42a59bfbd..7aa4bc30ce 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -130,7 +130,7 @@ val declare_include : (together with their section path). *) val iter_all_segments : - (Libnames.object_name -> Libobject.obj -> unit) -> unit + (Libobject.object_name -> Libobject.obj -> unit) -> unit val debug_print_modtab : unit -> Pp.t diff --git a/library/lib.ml b/library/lib.ml index 27c5056a7f..1acc8fd8fd 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -138,7 +138,7 @@ let make_kn id = let mp = current_mp () in Names.KerName.make mp (Names.Label.of_id id) -let make_oname id = Libnames.make_oname !lib_state.path_prefix id +let make_oname id = Libobject.make_oname !lib_state.path_prefix id let recalc_path_prefix () = let rec recalc = function diff --git a/library/lib.mli b/library/lib.mli index 686e6a0e2d..c6c6a307d4 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -25,7 +25,7 @@ type node = | OpenedModule of is_type * export * Libnames.object_prefix * Summary.frozen | OpenedSection of Libnames.object_prefix * Summary.frozen -type library_segment = (Libnames.object_name * node) list +type library_segment = (Libobject.object_name * node) list type lib_objects = (Id.t * Libobject.obj) list @@ -53,13 +53,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 : Id.t -> Libobject.obj -> Libnames.object_name +val add_leaf : Id.t -> Libobject.obj -> Libobject.object_name val add_anonymous_leaf : ?cache_first:bool -> Libobject.obj -> unit -val pull_to_head : Libnames.object_name -> unit +val pull_to_head : Libobject.object_name -> unit (** this operation adds all objects with the same name and calls [load_object] for each of them *) -val add_leaves : Id.t -> Libobject.obj list -> Libnames.object_name +val add_leaves : Id.t -> Libobject.obj list -> Libobject.object_name (** {6 ... } *) @@ -70,7 +70,7 @@ val contents : unit -> library_segment (** The function [contents_after] returns the current library segment, starting from a given section path. *) -val contents_after : Libnames.object_name -> library_segment +val contents_after : Libobject.object_name -> library_segment (** {6 Functions relative to current path } *) @@ -113,20 +113,20 @@ val start_modtype : val end_module : unit -> - Libnames.object_name * Libnames.object_prefix * + Libobject.object_name * Libnames.object_prefix * Summary.frozen * library_segment val end_modtype : unit -> - Libnames.object_name * Libnames.object_prefix * + Libobject.object_name * Libnames.object_prefix * Summary.frozen * library_segment (** {6 Compilation units } *) val start_compilation : DirPath.t -> ModPath.t -> unit -val end_compilation_checks : DirPath.t -> Libnames.object_name +val end_compilation_checks : DirPath.t -> Libobject.object_name val end_compilation : - Libnames.object_name-> Libnames.object_prefix * library_segment + Libobject.object_name-> Libnames.object_prefix * library_segment (** The function [library_dp] returns the [DirPath.t] of the current compiling library (or [default_library]) *) diff --git a/library/libnames.ml b/library/libnames.ml index bd2ca550b9..f6fc5ed4b7 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -162,18 +162,12 @@ let qualid_basename qid = let qualid_path qid = qid.CAst.v.dirpath -type object_name = full_path * KerName.t - type object_prefix = { obj_dir : DirPath.t; obj_mp : ModPath.t; obj_sec : DirPath.t; } -(* let make_oname (dirpath,(mp,dir)) id = *) -let make_oname { obj_dir; obj_mp } id = - make_path obj_dir id, KerName.make obj_mp (Label.of_id id) - (* to this type are mapped DirPath.t's in the nametab *) type global_dir_reference = | DirOpenModule of object_prefix diff --git a/library/libnames.mli b/library/libnames.mli index 447eecbb5c..9d75ec6e40 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -88,12 +88,6 @@ val qualid_is_ident : qualid -> bool val qualid_path : qualid -> DirPath.t val qualid_basename : qualid -> Id.t -(** Both names are passed to objects: a "semantic" [kernel_name], which - can be substituted and a "syntactic" [full_path] which can be printed -*) - -type object_name = full_path * KerName.t - (** Object prefix morally contains the "prefix" naming of an object to be stored by [library], where [obj_dir] is the "absolute" path, [obj_mp] is the current "module" prefix and [obj_sec] is the @@ -116,8 +110,6 @@ type object_prefix = { val eq_op : object_prefix -> object_prefix -> bool -val make_oname : object_prefix -> Id.t -> object_name - (** to this type are mapped [DirPath.t]'s in the nametab *) type global_dir_reference = | DirOpenModule of object_prefix diff --git a/library/libobject.ml b/library/libobject.ml index 79a3fed1b9..ea19fbb90b 100644 --- a/library/libobject.ml +++ b/library/libobject.ml @@ -16,6 +16,12 @@ module Dyn = Dyn.Make () type 'a substitutivity = Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a +type object_name = Libnames.full_path * Names.KerName.t + +(* let make_oname (dirpath,(mp,dir)) id = *) +let make_oname { obj_dir; obj_mp } id = + Names.(make_path obj_dir id, KerName.make obj_mp (Label.of_id id)) + type 'a object_declaration = { object_name : string; cache_function : object_name * 'a -> unit; diff --git a/library/libobject.mli b/library/libobject.mli index aefa81b225..c53537e654 100644 --- a/library/libobject.mli +++ b/library/libobject.mli @@ -66,6 +66,13 @@ open Mod_subst type 'a substitutivity = Dispose | Substitute of 'a | Keep of 'a | Anticipate of 'a +(** Both names are passed to objects: a "semantic" [kernel_name], which + can be substituted and a "syntactic" [full_path] which can be printed +*) + +type object_name = full_path * Names.KerName.t +val make_oname : object_prefix -> Names.Id.t -> object_name + type 'a object_declaration = { object_name : string; cache_function : object_name * 'a -> unit; diff --git a/printing/prettyp.mli b/printing/prettyp.mli index 58606db019..9213bc8561 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -19,7 +19,7 @@ val assumptions_for_print : Name.t list -> Termops.names_context val print_closed_sections : bool ref val print_context : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t -val print_library_entry : env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option +val print_library_entry : env -> Evd.evar_map -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option val print_full_context : env -> Evd.evar_map -> Pp.t val print_full_context_typ : env -> Evd.evar_map -> Pp.t val print_full_pure_context : env -> Evd.evar_map -> Pp.t @@ -89,7 +89,7 @@ type object_pr = { print_module : bool -> ModPath.t -> Pp.t; print_modtype : ModPath.t -> Pp.t; print_named_decl : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t; - print_library_entry : env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option; + print_library_entry : env -> Evd.evar_map -> bool -> (Libobject.object_name * Lib.node) -> Pp.t option; print_context : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t; print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t; |