fixed bug with aliases

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10896 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 4 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 646063519..7169d709f 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -342,10 +342,12 @@ let rec intern_library (dir, f) needed =
 and intern_mandatory_library (dir,_) needed =
   intern_library (try_locate_absolute_library dir) needed
 
-let recheck_library ~admit ~check =
-  let al = List.map (fun q -> fst(try_locate_qualified_library q)) admit in
-  let admit = List.fold_right library_dep al LibraryMap.empty in
-  let modl = List.map try_locate_qualified_library check in
+let recheck_library ~norec ~admit ~check =
+  let nrl = List.map (fun q -> fst(try_locate_qualified_library q)) norec in
+  let al =  List.map (fun q -> fst(try_locate_qualified_library q)) admit in
+  let admit = List.fold_right library_dep (nrl@al) LibraryMap.empty in
+  let admit = List.fold_right LibraryMap.remove nrl admit in
+  let modl = List.map try_locate_qualified_library (norec@check) in
   let needed = List.rev (List.fold_right intern_library modl []) in
   Flags.if_verbose msgnl (fnl()++hv 2 (str "Ordered list:" ++ fnl() ++
     prlist