diff options
| author | Pierre-Marie Pédrot | 2019-05-15 18:47:22 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-05-19 13:12:52 +0200 |
| commit | b1a3ea4855b1e150b2e677a6d5466458893d6c60 (patch) | |
| tree | c3fbaab76020273c063b7c7dac4326602d7e1f16 /library | |
| parent | e9c2bc9aaddd401d18d90411ff68644b1d05c0d5 (diff) | |
Inverting the responsibility to define logically a constant in Declare.
The code was intricate due to the special handling of side-effects, while
it was sufficient to extrude the logical definition to make it clearer. We
thus declare a constant in two parts, first purely kernel-related, then
purely libobject-related.
Diffstat (limited to 'library')
| -rw-r--r-- | library/lib.ml | 3 | ||||
| -rw-r--r-- | library/lib.mli | 1 |
2 files changed, 0 insertions, 4 deletions
diff --git a/library/lib.ml b/library/lib.ml index a046360822..4be288ed20 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -211,9 +211,6 @@ let split_lib_at_opening sp = let add_entry sp node = lib_state := { !lib_state with lib_stk = (sp,node) :: !lib_state.lib_stk } -let pull_to_head oname = - lib_state := { !lib_state with lib_stk = (oname,List.assoc oname !lib_state.lib_stk) :: List.remove_assoc oname !lib_state.lib_stk } - let anonymous_id = let n = ref 0 in fun () -> incr n; Names.Id.of_string ("_" ^ (string_of_int !n)) diff --git a/library/lib.mli b/library/lib.mli index 30569197bc..5da76961a6 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -57,7 +57,6 @@ val segment_of_objects : val add_leaf : Id.t -> Libobject.obj -> Libobject.object_name val add_anonymous_leaf : ?cache_first:bool -> Libobject.obj -> 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 *) |