aboutsummaryrefslogtreecommitdiff
path: root/contrib/interface/parse.ml
diff options
context:
space:
mode:
authorherbelin2005-02-06 13:03:51 +0000
committerherbelin2005-02-06 13:03:51 +0000
commita608c8e1bffa032ed67f6f2dd406017b6aca9eb9 (patch)
tree5bb5097ecebd3d07d1749af17520a77f6d2b6a4a /contrib/interface/parse.ml
parentf937000d0093a1cae137753f6e73ec15561cb9df (diff)
Nettoyage et documentation de Library
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6692 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface/parse.ml')
-rw-r--r--contrib/interface/parse.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml
index 6a99aedc8c..a6a8937ba5 100644
--- a/contrib/interface/parse.ml
+++ b/contrib/interface/parse.ml
@@ -401,7 +401,7 @@ let load_syntax_action reqid module_name =
msg (str "loading " ++ str module_name ++ str "... ");
try
(let qid = Libnames.make_short_qualid (Names.id_of_string module_name) in
- read_library (dummy_loc,qid);
+ require_library [dummy_loc,qid] None;
msg (str "opening... ");
Declaremods.import_module false (Nametab.locate_module qid);
msgnl (str "done" ++ fnl ());