diff options
| -rw-r--r-- | library/declaremods.ml | 2 | ||||
| -rw-r--r-- | library/lib.ml | 6 | ||||
| -rw-r--r-- | library/lib.mli | 10 | ||||
| -rw-r--r-- | plugins/extraction/extract_env.ml | 3 | ||||
| -rw-r--r-- | printing/prettyp.ml | 13 |
5 files changed, 17 insertions, 17 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml index a5804eb53..0a5b61656 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -920,7 +920,7 @@ let iter_all_segments f = | sp, Leaf o -> f sp o | _ -> () in - List.iter apply_node (Lib.contents_after None) + List.iter apply_node (Lib.contents ()) let debug_print_modtab _ = diff --git a/library/lib.ml b/library/lib.ml index bf4c0a474..47341e675 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -312,9 +312,9 @@ let end_mod is_type = let end_module () = end_mod false let end_modtype () = end_mod true -let contents_after = function - | None -> !lib_stk - | Some sp -> let (after,_,_) = split_lib sp in after +let contents () = !lib_stk + +let contents_after sp = let (after,_,_) = split_lib sp in after (* Modules. *) diff --git a/library/lib.mli b/library/lib.mli index c9b2047bc..a956ff5d0 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -63,11 +63,15 @@ val add_leaves : Names.Id.t -> Libobject.obj list -> Libnames.object_name val add_frozen_state : unit -> unit (** {6 ... } *) + +(** The function [contents] gives access to the current entire segment *) + +val contents : unit -> library_segment + (** The function [contents_after] returns the current library segment, - starting from a given section path. If not given, the entire segment - is returned. *) + starting from a given section path. *) -val contents_after : Libnames.object_name option -> library_segment +val contents_after : Libnames.object_name -> library_segment (** {6 Functions relative to current path } *) diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index fae5c7e67..cc302b95d 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -26,7 +26,6 @@ open Mod_subst (***************************************) let toplevel_env () = - let seg = Lib.contents_after None in let get_reference = function | (_,kn), Lib.Leaf o -> let mp,_,l = repr_kn kn in @@ -48,7 +47,7 @@ let toplevel_env () = end | _ -> None in - SEBstruct (List.rev (List.map_filter get_reference seg)) + SEBstruct (List.rev (List.map_filter get_reference (Lib.contents ()))) let environment_until dir_opt = diff --git a/printing/prettyp.ml b/printing/prettyp.ml index bc9137ede..d7d7bd97d 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -547,11 +547,8 @@ let print_safe_judgment env j = (*********************) (* *) -let print_full_context () = - print_context true None (Lib.contents_after None) - -let print_full_context_typ () = - print_context false None (Lib.contents_after None) +let print_full_context () = print_context true None (Lib.contents ()) +let print_full_context_typ () = print_context false None (Lib.contents ()) let print_full_pure_context () = let rec prec = function @@ -593,7 +590,7 @@ let print_full_pure_context () = prec rest ++ pp | _::rest -> prec rest | _ -> mt () in - prec (Lib.contents_after None) + prec (Lib.contents ()) (* For printing an inductive definition with its constructors and elimination, @@ -616,7 +613,7 @@ let read_sec_context r = | [] -> [] | hd::rest -> get_cxt (hd::in_cxt) rest in - let cxt = (Lib.contents_after None) in + let cxt = Lib.contents () in List.rev (get_cxt [] cxt) let print_sec_context sec = @@ -700,7 +697,7 @@ let print_about = function (* for debug *) let inspect depth = - print_context false (Some depth) (Lib.contents_after None) + print_context false (Some depth) (Lib.contents ()) (*************************************************************************) |