diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-14 00:17:06 +0100 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-03-14 00:17:06 +0100 |
commit | bbae426407ba7df585c22ec687a79c0cf216a6a8 (patch) | |
tree | 3005a61d1997d772a9bb8be5389408f933d46033 /library | |
parent | ecacc9af6100f76e95acc24e777026bfc9c4d921 (diff) |
[library] Don't recompute path_prefix on unfreeze.
We instead save the current value.
Diffstat (limited to 'library')
-rw-r--r-- | library/lib.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/library/lib.ml b/library/lib.ml index 4fd29a94d..1531d408f 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -561,7 +561,7 @@ let close_section () = (* State and initialization. *) -type frozen = Names.DirPath.t option * library_segment +type frozen = Names.DirPath.t option * library_segment * (Names.DirPath.t * (Names.module_path * Names.DirPath.t)) let freeze ~marshallable = match marshallable with @@ -579,17 +579,17 @@ let freeze ~marshallable = | n, ClosedSection _ -> Some (n,ClosedSection []) | _, FrozenState _ -> None) !lib_stk in - !comp_name, lib_stk + !comp_name, lib_stk, !path_prefix | _ -> - !comp_name, !lib_stk + !comp_name, !lib_stk, !path_prefix -let unfreeze (mn,stk) = +let unfreeze (mn,stk,path_prfx) = comp_name := mn; lib_stk := stk; - recalc_path_prefix () + path_prefix := path_prfx let init () = - unfreeze (None,[]); + unfreeze (None,[],initial_prefix); Summary.init_summaries (); add_frozen_state () (* Stores e.g. the keywords declared in g_*.ml4 *) |