diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-07 21:32:07 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-07 21:32:07 +0000 |
| commit | bc6787e51fdb3b2bb449d288791e963dd7416737 (patch) | |
| tree | 6bad12ec21d64fc4e520b46edae97cfe63ba6342 /toplevel | |
| parent | 7d122040f6eacbe7e96898f7df86163847e762ed (diff) | |
Meilleure approche du conflit path/freeze/library_root en séquentialisant la partie asynchrone (path) de la partie synchrone (roots)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1351 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqinit.ml | 7 | ||||
| -rw-r--r-- | toplevel/coqinit.mli | 1 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 1 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 9 |
4 files changed, 14 insertions, 4 deletions
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 8d45151b2..da86562f0 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -84,6 +84,9 @@ let init_load_path () = List.iter (fun (s,alias,reci) -> if reci then Mltop.add_rec_path s alias else Mltop.add_path s alias) - (List.rev !includes); - includes := [] + (List.rev !includes) +let init_library_roots () = + List.iter + (fun (_,alias,_) -> Nametab.push_library_root (List.hd alias)) !includes; + includes := [] diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index a0b3d5911..f81d88eae 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -15,3 +15,4 @@ val push_include : string * Names.dir_path -> unit val push_rec_include : string * Names.dir_path -> unit val init_load_path : unit -> unit +val init_library_roots : unit -> unit diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 5ece34630..3d809508b 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -184,6 +184,7 @@ let start () = if is_verbose() then print_header (); init_load_path (); inputstate (); + init_library_roots (); load_vernac_obj (); require (); load_rcfile(); diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 9e53e01c4..153e91667 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -198,10 +198,15 @@ let _ = let alias = Filename.basename dir in if alias = "" then error ("Cannot map "^dir^" to a root of Coq library"); - (fun () -> add_rec_path dir [alias]) + (fun () -> + add_rec_path dir [alias]; + Nametab.push_library_root alias) | [VARG_STRING dir ; VARG_QUALID alias] -> let aliasdir,aliasname = repr_qualid alias in - (fun () -> add_rec_path dir (aliasdir@[aliasname])) + (fun () -> + let alias = aliasdir@[aliasname] in + add_rec_path dir alias; + Nametab.push_library_root (List.hd alias)) | _ -> bad_vernac_args "RECADDPATH") (* For compatibility *) |