fixed bug #1927 + univ constraints (module cstrs include cstrs of its subcomponents)

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

1 files changed, 5 insertions, 3 deletions

diff --git a/checker/check.ml b/checker/check.ml
index e91516c7b..40ac604e0 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -23,8 +23,7 @@ type section_path = {
   dirpath : string list ;
   basename : string }
 let dir_of_path p =
-  make_dirpath
-    (id_of_string p.basename :: List.map id_of_string p.dirpath)
+  make_dirpath (List.map id_of_string p.dirpath)
 let path_of_dirpath dir = 
   match repr_dirpath dir with
       [] -> failwith "path_of_dirpath"
@@ -166,6 +165,9 @@ let remove_load_path dir =
   load_paths := list_filter2 (fun p d -> p <> dir) !load_paths
 
 let add_load_path (phys_path,coq_path) =
+  if !Flags.debug then
+    msgnl (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++
+           str phys_path);
   let phys_path = canonical_path_name phys_path in
     match list_filter2 (fun p d -> p = phys_path) !load_paths with
       | _,[dir] ->
@@ -224,7 +226,7 @@ let locate_qualified_library qid =
       (* Search library in loadpath *)
       if qid.dirpath=[] then get_load_paths ()
       else
-        (* we assume dir is an absolute dirpath *)
+        (* we assume qid is an absolute dirpath *)
         load_paths_of_dir_path (dir_of_path qid)
     in
     if loadpath = [] then raise LibUnmappedDir;