diff options
| author | coq | 2002-08-02 17:17:42 +0000 |
|---|---|---|
| committer | coq | 2002-08-02 17:17:42 +0000 |
| commit | 12965209478bd99dfbe57f07d5b525e51b903f22 (patch) | |
| tree | 36a7f5e4802cd321caf02fed0be8349100be09fb /contrib/interface/parse.ml | |
| parent | 8b26fd6ba739d4f49fae99ed764b086022e44b50 (diff) | |
Modules dans COQ\!\!\!\!
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface/parse.ml')
| -rw-r--r-- | contrib/interface/parse.ml | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml index 5bce60f223..61fd060724 100644 --- a/contrib/interface/parse.ml +++ b/contrib/interface/parse.ml @@ -6,6 +6,8 @@ open Ctast;; open Pp;; +open Libnames;; + open Library;; open Ascent;; @@ -67,7 +69,7 @@ let try_require_module import specif names = else Some (specif = "SPECIFICATION")) (List.map (fun name -> - (dummy_loc,Nametab.make_short_qualid (Names.id_of_string name))) + (dummy_loc,Libnames.make_short_qualid (Names.id_of_string name))) names) (import = "IMPORT") with @@ -110,7 +112,7 @@ let execute_when_necessary v = (try Vernacentries.interp v with _ -> - let l=prlist_with_sep spc (fun (_,qid) -> Nametab.pr_qualid qid) l in + let l=prlist_with_sep spc (fun (_,qid) -> pr_qualid qid) l in msgnl (str "Reinterning of " ++ l ++ str " failed")) | VernacRequireFrom (_,_,name,_) -> (try @@ -427,10 +429,10 @@ let print_version_action () = let load_syntax_action reqid module_name = msg (str "loading " ++ str module_name ++ str "... "); try - (let qid = Nametab.make_short_qualid (Names.id_of_string module_name) in - read_module (dummy_loc,qid); + (let qid = Libnames.make_short_qualid (Names.id_of_string module_name) in + read_library (dummy_loc,qid); msg (str "opening... "); - import_module false (dummy_loc,qid); + Declaremods.import_module (Nametab.locate_module qid); msgnl (str "done" ++ fnl ()); ()) with |