From 92ebdaa1a4f468d67fd583ebbf3aecf7ef3ece27 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sat, 4 Oct 2003 21:21:31 +0000 Subject: Reparation plus juste de l'inefficacite avec loaded_modules (respecte l'ordre) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4527 85f007b7-540e-0410-9357-904b9bb8a0f7 --- toplevel/mltop.ml4 | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'toplevel/mltop.ml4') diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index fec06f6e8..df40b6aa3 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -224,20 +224,20 @@ let load_object mname fname= (* List and not Stringset because order is important *) let loaded_modules = ref [] let get_loaded_modules () = !loaded_modules -let add_loaded_module md = - loaded_modules := md :: list_except md !loaded_modules +let add_loaded_module md = loaded_modules := md :: !loaded_modules let orig_loaded_modules = ref !loaded_modules let init_ml_modules () = loaded_modules := !orig_loaded_modules let unfreeze_ml_modules x = + loaded_modules := []; List.iter (fun name -> let mname = mod_of_name name in if not (module_is_known mname) then if enable_load() then let fname = file_of_name mname in - load_object mname fname + load_object mname fname else errorlabstrm "Mltop.unfreeze_ml_modules" [< str"Loading of ML object file forbidden in a native Coq" >]; -- cgit v1.2.3