- coq_makefile: target install now respects the original tree structure

  of the archive to install in coq user-contrib installation directory.
- Relaxed the validity check on identifiers from an error to a warning.
- Added a filtering option to Print LoadPath.
- Support for empty root in option -R.
- Better handling of redundant paths in ml loadpath.
- Makefile's: Added target initplugins and added initplugins to coqbinaries.



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

20 files changed, 317 insertions, 194 deletions

diff --git a/CHANGES b/CHANGES
index 395b4cf70..20b3131c4 100644
--- a/CHANGES
+++ b/CHANGES
@@ -82,6 +82,7 @@ Vernacular commands
   compiled in native code with a version of OCaml that supports native
   Dynlink (>= 3.11).
 - Specific sort constraints on Record now taken into account.
+- "Print LoadPath" supports a path argument to filter the display.
 
 Libraries (DOC TO CHECK)
 
diff --git a/Makefile.build b/Makefile.build
index fefaf2cb7..6a0857ccd 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -165,13 +165,13 @@ kernel/copcodes.ml: kernel/byterun/coq_instruct.h
 # Main targets (coqmktop, coqtop.opt, coqtop.byte)
 ###########################################################################
 
-coqbinaries:: ${COQBINARIES} ${CSDPCERT}
+coqbinaries:: ${COQBINARIES} ${CSDPCERT} $(INITPLUGINSOPT) $(INITPLUGINS)
 
 coq: coqlib tools coqbinaries
 
 coqlib:: initplugins theories contrib
 
-coqlight: initplugins theories-light tools coqbinaries
+coqlight: theories-light tools coqbinaries
 
 states:: states/initial.coq
 
diff --git a/Makefile.common b/Makefile.common
index c2f3e305b..b5c81882f 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -911,7 +911,7 @@ STAGE2_TARGETS:=$(COQBINARIES) lib kernel byterun library proofs tactics \
   interp parsing pretyping highparsing toplevel hightactics \
   coqide-binaries coqide-byte coqide-opt $(COQIDEOPT) $(COQIDEBYTE) $(COQIDE) \
   pcoq-binaries $(COQINTERFACE) $(CSDPCERT) coqbinaries pcoq $(TOOLS) tools \
-  printers debug
+  printers debug initplugins
 VO_TARGETS:=logic arith bool narith zarith qarith lists strings sets \
   fsets allfsets relations wellfounded ints reals allreals \
   setoids sorting natural integer rational numbers noreal \
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 6d6a0c065..02f36a8c8 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1886,7 +1886,8 @@ let rec xlate_vernac =
 	| PrintHint id ->
 	    CT_print_hint (CT_coerce_ID_to_ID_OPT (loc_qualid_to_ct_ID id))
 	| PrintHintGoal -> CT_print_hint ctv_ID_OPT_NONE
-	| PrintLoadPath -> CT_print_loadpath
+	| PrintLoadPath None -> CT_print_loadpath
+	| PrintLoadPath _ -> xlate_error "TODO: Print LoadPath dir"
 	| PrintMLLoadPath -> CT_ml_print_path
 	| PrintMLModules -> CT_ml_print_modules
 	| PrintGraph -> CT_print_graph
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 6db166762..3f1e517d6 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -629,6 +629,11 @@ This command removes the path {\str} from the current \Coq\ loadpath.
 \subsection[\tt Print LoadPath.]{\tt Print LoadPath.\comindex{Print LoadPath}}
 This command displays the current \Coq\ loadpath.
 
+\begin{Variants}
+\item {\tt Print LoadPath {\dirpath}.}\\
+Works as {\tt Print LoadPath} but displays only the paths that extend the {\dirpath} prefix.
+\end{Variants}
+
 \subsection[\tt Add ML Path {\str}.]{\tt Add ML Path {\str}.\comindex{Add ML Path}}
 This command adds the path {\str} to the current Objective Caml loadpath (see
 the command {\tt Declare ML Module} in the Section~\ref{compiled}).
diff --git a/kernel/names.ml b/kernel/names.ml
index e75900cfa..6ee96fddd 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -17,7 +17,7 @@ type identifier = string
 
 let id_ord = Pervasives.compare
 
-let id_of_string s = check_ident s; String.copy s
+let id_of_string s = check_ident_soft s; String.copy s
 
 let string_of_id id = String.copy id
 
diff --git a/lib/system.ml b/lib/system.ml
index 7ca62dcc8..00d6dec22 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -63,6 +63,34 @@ type load_path = physical_path list
 let physical_path_of_string s = s
 let string_of_physical_path p = p
 
+(* Hints to partially detects if two paths refer to the same repertory *)
+let rec remove_path_dot p = 
+  let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *)
+  let n = String.length curdir in
+  if String.length p > n && String.sub p 0 n = curdir then
+    remove_path_dot (String.sub p n (String.length p - n))
+  else
+    p
+
+let strip_path p =
+  let cwd = Filename.concat (Sys.getcwd ()) "" in (* Unix: "`pwd`/" *)
+  let n = String.length cwd in
+  if String.length p > n && String.sub p 0 n = cwd then
+    remove_path_dot (String.sub p n (String.length p - n))
+  else
+    remove_path_dot p
+
+let canonical_path_name p =
+  let current = Sys.getcwd () in
+  try 
+    Sys.chdir p;
+    let p' = Sys.getcwd () in
+    Sys.chdir current;
+    p'
+  with Sys_error _ ->
+    (* We give up to find a canonical name and just simplify it... *)
+    strip_path p
+
 (* All subdirectories, recursively *)
 
 let exists_dir dir =
diff --git a/lib/system.mli b/lib/system.mli
index 6c607607f..48e02cb5d 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -16,6 +16,8 @@
 type physical_path = string
 type load_path = physical_path list
 
+val canonical_path_name : string -> string
+
 val exclude_search_in_dirname : string -> unit
 
 val all_subdirs : unix_path:string -> (physical_path * string list) list
diff --git a/lib/util.ml b/lib/util.ml
index b0e66af05..3b04e2574 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -309,27 +309,40 @@ let next_utf8 s i =
 
 (* Check the well-formedness of an identifier *)
 
-let check_ident s =
+let check_initial handle j n s =
+  match classify_unicode n with
+  | UnicodeLetter -> ()
+  | _ ->
+      let c = String.sub s 0 j in
+      handle ("Invalid character '"^c^"' at beginning of identifier \""^s^"\".")
+
+let check_trailing handle i j n s =
+  match classify_unicode n with
+  | UnicodeLetter | UnicodeIdentPart -> ()
+  | _ ->
+      let c = String.sub s i j in
+      handle ("Invalid character '"^c^"' in identifier \""^s^"\".")
+
+let check_ident_gen handle s =
   let i = ref 0 in
   if s <> ".." then try
     let j, n = next_utf8 s 0 in
-    match classify_unicode n with
-    | UnicodeLetter ->
-	i := !i + j;
-	begin try
-	  while true do
-	    let j, n = next_utf8 s !i in
-	    match classify_unicode n with
-	    | UnicodeLetter | UnicodeIdentPart -> i := !i + j
-	    | _ -> error
-		("invalid character "^(String.sub s !i j)^" in identifier "^s)
-	  done
-	with End_of_input -> () end
-    | _ -> error (s^": an identifier should start with a letter")
+    check_initial handle j n s;
+    i := !i + j;
+    try
+      while true do
+	let j, n = next_utf8 s !i in
+	check_trailing handle !i j n s;
+	i := !i + j
+      done
+    with End_of_input -> ()
   with 
-  | End_of_input -> error "The empty string is not an identifier"
-  | UnsupportedUtf8 -> error (s^": unsupported character in utf8 sequence")
-  | Invalid_argument _ -> error (s^": invalid utf8 sequence")
+  | End_of_input -> error "The empty string is not an identifier."
+  | UnsupportedUtf8 -> error (s^": unsupported character in utf8 sequence.")
+  | Invalid_argument _ -> error (s^": invalid utf8 sequence.")
+
+let check_ident_soft = check_ident_gen warning
+let check_ident = check_ident_gen error
 
 let lowercase_unicode s unicode =
     match unicode land 0x1F000 with
diff --git a/lib/util.mli b/lib/util.mli
index 8b27e6158..dc6498b15 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -89,6 +89,7 @@ exception UnsupportedUtf8
 
 val classify_unicode : int -> utf8_status
 val check_ident : string -> unit
+val check_ident_soft : string -> unit
 val lowercase_first_char_utf8 : string -> string
 
 (*s Lists. *)
diff --git a/library/libnames.ml b/library/libnames.ml
index bf02efb03..b7b36afb3 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -123,21 +123,21 @@ let path_of_inductive env (sp,tyi) =
 let parse_dir s =
   let len = String.length s in
   let rec decoupe_dirs dirs n =
-    if n>=len then dirs else
+    if n = len && n > 0 then error (s ^ " is an invalid path.");
+    if n >= len then dirs else
     let pos =
       try
 	String.index_from s n '.' 
       with Not_found -> len
     in
+    if pos = n then error (s ^ " is an invalid path.");
     let dir = String.sub s n (pos-n) in
-      decoupe_dirs ((id_of_string dir)::dirs) (pos+1)	  
+    decoupe_dirs ((id_of_string dir)::dirs) (pos+1)	  
   in
     decoupe_dirs [] 0
 
-let dirpath_of_string s = 
-  match parse_dir s with
-      [] -> invalid_arg "dirpath_of_string"
-    | dir -> make_dirpath dir
+let dirpath_of_string s =
+  make_dirpath (if s = "" then [] else parse_dir s)
 
 module Dirset = Set.Make(struct type t = dir_path let compare = compare end)
 module Dirmap = Map.Make(struct type t = dir_path let compare = compare end)
diff --git a/library/library.ml b/library/library.ml
index fd9d93eb4..ff0e62064 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -28,43 +28,15 @@ let load_paths = ref ([] : (System.physical_path * logical_path * bool) list)
 
 let get_load_paths () = List.map pi1 !load_paths
 
-(* Hints to partially detects if two paths refer to the same repertory *)
-let rec remove_path_dot p = 
-  let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *)
-  let n = String.length curdir in
-  if String.length p > n && String.sub p 0 n = curdir then
-    remove_path_dot (String.sub p n (String.length p - n))
-  else
-    p
-
-let strip_path p =
-  let cwd = Filename.concat (Sys.getcwd ()) "" in (* Unix: "`pwd`/" *)
-  let n = String.length cwd in
-  if String.length p > n && String.sub p 0 n = cwd then
-    remove_path_dot (String.sub p n (String.length p - n))
-  else
-    remove_path_dot p
-
-let canonical_path_name p =
-  let current = Sys.getcwd () in
-  try 
-    Sys.chdir p;
-    let p' = Sys.getcwd () in
-    Sys.chdir current;
-    p'
-  with Sys_error _ ->
-    (* We give up to find a canonical name and just simplify it... *)
-    strip_path p
-
 let find_logical_path phys_dir =
-  let phys_dir = canonical_path_name phys_dir in
+  let phys_dir = System.canonical_path_name phys_dir in
   match List.filter (fun (p,d,_) -> p = phys_dir) !load_paths with
   | [_,dir,_] -> dir
   | [] -> Nameops.default_root_prefix
   | l -> anomaly ("Two logical paths are associated to "^phys_dir)
 
 let is_in_load_paths phys_dir =
-  let dir = canonical_path_name phys_dir in
+  let dir = System.canonical_path_name phys_dir in
   let lp = get_load_paths () in
   let check_p = fun p -> (String.compare dir p) == 0 in
     List.exists check_p lp 
@@ -73,13 +45,13 @@ let remove_load_path dir =
   load_paths := List.filter (fun (p,d,_) -> p <> dir) !load_paths
 
 let add_load_path isroot (phys_path,coq_path) =
-  let phys_path = canonical_path_name phys_path in
+  let phys_path = System.canonical_path_name phys_path in
     match List.filter (fun (p,d,_) -> p = phys_path) !load_paths with
       | [_,dir,_] ->
 	  if coq_path <> dir 
             (* If this is not the default -I . to coqtop *)
             && not
-            (phys_path = canonical_path_name Filename.current_dir_name
+            (phys_path = System.canonical_path_name Filename.current_dir_name
 		&& coq_path = Nameops.default_root_prefix)
 	  then
 	    begin
@@ -627,9 +599,15 @@ let import_module export (loc,qid) =
 (************************************************************************)
 (*s Initializing the compilation of a library. *)
 
+let check_coq_overwriting p =
+  let l = repr_dirpath p in
+  if not !Flags.boot && l <> [] && string_of_id (list_last l) = "Coq" then
+    errorlabstrm "" (strbrk ("Name "^string_of_dirpath p^" starts with prefix \"Coq\" which is reserved for the Coq library."))
+
 let start_library f = 
   let _,longf = System.find_file_in_path (get_load_paths ()) (f^".v") in
   let ldir0 = find_logical_path (Filename.dirname longf) in
+  check_coq_overwriting ldir0;
   let id = id_of_string (Filename.basename f) in
   let ldir = extend_dirpath ldir0 id in
   Declaremods.start_library ldir;
diff --git a/library/library.mli b/library/library.mli
index c6bd8fe0b..2b7ecc664 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -79,5 +79,8 @@ val locate_qualified_library :
   bool -> qualid -> library_location * dir_path * System.physical_path
 val try_locate_qualified_library : qualid located -> dir_path * string
 
+(* Reserve Coq prefix for the standard library *)
+val check_coq_overwriting : dir_path -> unit
+
 (*s Statistics: display the memory use of a library. *)
 val mem : dir_path -> Pp.std_ppcmds
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 4ffd53fe4..48a7a7a5a 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -675,7 +675,7 @@ GEXTEND Gram
       | IDENT "Grammar"; ent = IDENT ->
           (* This should be in "syntax" section but is here for factorization*)
 	  PrintGrammar ent
-      | IDENT "LoadPath" -> PrintLoadPath
+      | IDENT "LoadPath"; dir = OPT dirpath -> PrintLoadPath dir
       | IDENT "Modules" -> 
           error "Print Modules is obsolete; use Print Libraries instead"
       | IDENT "Libraries" -> PrintModules
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 33c7654d2..a3eed62b7 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -878,7 +878,7 @@ let rec pr_vernac = function
             str"Print Section" ++ spc() ++ Libnames.pr_reference s
 	| PrintGrammar ent ->
             str"Print Grammar" ++ spc() ++ str ent
-	| PrintLoadPath -> str"Print LoadPath"
+	| PrintLoadPath dir -> str"Print LoadPath" ++ pr_opt pr_dirpath dir
 	| PrintModules -> str"Print Modules"
 	| PrintMLLoadPath -> str"Print ML Path"
 	| PrintMLModules -> str"Print ML Modules"
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index 77fdffb0d..dcb220ea2 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -29,6 +29,7 @@ let some_mlfile = ref false
 
 let opt = ref "-opt"
 let impredicative_set = ref false
+let no_install = ref false
 
 let print x = output_string !output_channel x
 let printf x = Printf.fprintf !output_channel x
@@ -38,6 +39,9 @@ let rec print_list sep = function
   | x :: l -> print x; print sep; print_list sep l
   | [] -> ()
 
+let list_iter_i f =
+  let rec aux i = function [] -> () | a::l -> f i a; aux (i+1) l in aux 1
+
 let best_ocamlc = 
   if Coq_config.best = "opt" then "ocamlc.opt" else "ocamlc"
 let best_ocamlopt =
@@ -63,10 +67,11 @@ let usage () =
 
 coq_makefile [subdirectory] .... [file.v] ... [file.ml] ... [-custom
   command dependencies file] ... [-I dir] ... [-R physicalpath logicalpath]
-  ... [VARIABLE = value] ...  [-opt|-byte] [-f file] [-o file] [-h] [--help]
+  ... [VARIABLE = value] ...  [-opt|-byte] [-impredicative-set] [-no-install]
+  [-f file] [-o file] [-h] [--help]
 
 [file.v]: Coq file to be compiled
-[file.ml]: ML file to be compiled
+[file.ml]: Objective Caml file to be compiled
 [subdirectory] : subdirectory that should be \"made\"
 [-custom command dependencies file]: add target \"file\" with command
   \"command\" and dependencies \"dependencies\"
@@ -78,6 +83,7 @@ coq_makefile [subdirectory] .... [file.v] ... [file.ml] ... [-custom
 [-byte]: compile with byte-code version of coq
 [-opt]: compile with native-code version of coq
 [-impredicative-set]: compile with option -impredicative-set of coq
+[-no-install]: build a makefile with no install target
 [-f file]: take the contents of file as arguments
 [-o file]: output should go in file file 
 [-h]: print this usage summary
@@ -88,24 +94,106 @@ let is_genrule r =
     let genrule = Str.regexp("%") in
       Str.string_match genrule r 0
 
-let standard sds sps =
+let absolute_dir dir =
+  let current = Sys.getcwd () in
+    Sys.chdir dir;
+    let dir' = Sys.getcwd () in
+      Sys.chdir current;
+      dir'
+
+let is_prefix dir1 dir2 =
+  let l1 = String.length dir1 in
+  let l2 = String.length dir2 in
+    dir1 = dir2 or (l1 < l2 & String.sub dir2 0 l1 = dir1 & dir2.[l1] = '/')
+
+let canonize f =
+  let l = String.length f in
+  if l > 2 && f.[0] = '.' && f.[1] = '/' then
+    let n = let i = ref 2 in while !i < l && f.[!i] = '/' do incr i done; !i in
+    String.sub f n (l-n)
+  else f
+
+let is_absolute_prefix dir dir' =
+  is_prefix (absolute_dir dir) (absolute_dir dir')
+
+let is_included dir = function
+  | RInclude (dir',_) -> is_absolute_prefix dir' dir
+  | Include dir' -> absolute_dir dir = absolute_dir dir'
+  | _ -> false
+
+let has_top_file = function
+  | ML s | V s -> s = Filename.basename s
+  | _ -> false
+
+let physical_dir_of_logical_dir ldir =
+  let pdir = String.copy ldir in
+  for i = 0 to String.length ldir - 1 do
+    if pdir.[i] = '.' then pdir.[i] <- '/';
+  done;
+  pdir
+
+let standard ()=
   print "byte:\n";
   print "\t$(MAKE) all \"OPT:=-byte\"\n\n";
   print "opt:\n";
   if !opt = "" then print "\t@echo \"WARNING: opt is disabled\"\n";
-  print "\t$(MAKE) all \"OPT:="; print !opt; print "\"\n\n";
+  print "\t$(MAKE) all \"OPT:="; print !opt; print "\"\n\n"
+
+let is_prefix_of_file dir f =
+  is_prefix dir (absolute_dir (Filename.dirname f))
+
+let classify_files_by_root var files (inc_i,inc_r) =
+  if not (List.exists (fun (pdir,_,_) -> pdir = ".") inc_r) then
+    begin
+      (* Files in the scope of a -R option (assuming they are disjoint) *)
+      list_iter_i (fun i (pdir,ldir,abspdir) ->
+	if List.exists (is_prefix_of_file abspdir) files then
+	  printf "%s%d:=$(patsubst %s/%%,%%,$(filter %s/%%,$(%s)))\n"
+	    var i pdir pdir var)
+	inc_r;
+      (* Files not in the scope of a -R option *)
+      let pat_of_dir (pdir,_,_) = pdir^"/%" in
+      let pdir_patterns = String.concat " " (List.map pat_of_dir inc_r) in
+      printf "%s0:=$(filter-out %s,$(%s))\n" var pdir_patterns var
+    end
+
+let install_include_by_root var files (_,inc_r) =
+  try
+    (* All files caught by a -R . option (assuming it is the only one) *)
+    let ldir = List.assoc "." (List.map (fun (p,l,_) -> (p,l)) inc_r) in
+    let pdir = physical_dir_of_logical_dir ldir in
+    printf "\t(for i in $(%s); do \\\n" var;
+    printf "\t install -D $$i $(COQLIB)/user-contrib/%s/$$i; \\\n" pdir;
+    printf "\t done)\n"
+  with Not_found ->
+    (* Files in the scope of a -R option (assuming they are disjoint) *)
+    list_iter_i (fun i (pdir,ldir,abspdir) ->
+      if List.exists (is_prefix_of_file abspdir) files then
+	begin
+	  let pdir' = physical_dir_of_logical_dir ldir in
+	  printf "\t(cd %s; for i in $(%s%d); do \\\n" pdir var i;
+	  printf "\t install -D $$i $(COQLIB)/user-contrib/%s/$$i; \\\n" pdir';
+	  printf "\t done)\n"
+	end) inc_r;
+    (* Files not in the scope of a -R option *)
+    printf "\t(for i in $(%s0); do \\\n" var;
+    printf "\t install -D $$i $(COQLIB)/user-contrib/$(INSTALLDEFAULTROOT)/$$i; \\\n";
+    printf "\t done)\n"
+
+let install (vfiles,mlfiles,_,sds) inc =
   print "install:\n";
   print "\tmkdir -p $(COQLIB)/user-contrib\n";
-  if !some_vfile then
-    print "\tcp -f $(VOFILES) $(COQLIB)/user-contrib\n";
-  if !some_mlfile then
-    print "\tcp -f $(CMOFILES) $(COQLIB)/user-contrib\n";
+  if !some_vfile then install_include_by_root "VOFILES" vfiles inc;
+  if !some_mlfile then install_include_by_root "CMOFILES" mlfiles inc;
   if Coq_config.has_natdynlink && !some_mlfile then
-    print "\tcp -f $(CMXSFILES) $(COQLIB)/user-contrib\n";
+    install_include_by_root "CMXSFILES" mlfiles inc;
   List.iter
-    (fun x -> print "\t(cd "; print x; print " ; $(MAKE) install)\n")
+    (fun x ->
+      printf "\t(cd %s; $(MAKE) INSTALLDEFAULTROOT=$(INSTALLDEFAULTROOT)/%s install)\n" x x)
     sds;
-  print "\n";
+  print "\n"
+
+let make_makefile sds =
   if !make_name <> "" then begin
     printf "%s: %s\n" !makefile_name !make_name;
     printf "\tmv -f %s %s.bak\n" !makefile_name !makefile_name;
@@ -115,7 +203,9 @@ let standard sds sps =
       (fun x -> print "\t(cd "; print x; print " ; $(MAKE) Makefile)\n")
       sds;
     print "\n";
-  end;
+  end
+
+let clean sds sps =
   print "clean:\n";
   print "\trm -f $(CMOFILES) $(CMIFILES) $(CMXFILES) $(CMXSFILES) $(OFILES) $(VOFILES) $(VIFILES) $(GFILES) $(MLFILES:.ml=.cmo) $(MLFILES:.ml=.cmx) *~\n";
   print "\trm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(HTMLFILES) \
@@ -171,12 +261,8 @@ let implicit () =
     if !some_mlfile then ml_rules ();
     if !some_vfile then v_rule ()
 
-let variables l =
-  let rec var_aux = function
-    | [] -> ()
-    | Def(v,def) :: r -> print v; print "="; print def; print "\n"; var_aux r
-    | _ :: r -> var_aux r
-  in
+let variables defs =
+  let var_aux (v,def) = print v; print "="; print def; print "\n" in
     section "Variables definitions.";
     print "ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)\n";
     if !opt = "-byte" then 
@@ -200,33 +286,10 @@ let variables l =
     print "GRAMMARS:=grammar.cma\n";
     print "CAMLP4EXTEND:=pa_extend.cmo pa_macro.cmo q_MLast.cmo\n";
     print "CAMLP4OPTIONS:=\n";
-    var_aux l;
+    List.iter var_aux defs;
     print "PP:=-pp \"$(CAMLP4BIN)$(CAMLP4)o -I . $(COQSRCLIBS) $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl\"\n";
     print "\n"
 
-let absolute_dir dir =
-  let current = Sys.getcwd () in
-    Sys.chdir dir;
-    let dir' = Sys.getcwd () in
-      Sys.chdir current;
-      dir'
-
-let is_prefix dir1 dir2 =
-  let l1 = String.length dir1 in
-  let l2 = String.length dir2 in
-    dir1 = dir2 or (l1 < l2 & String.sub dir2 0 l1 = dir1 & dir2.[l1] = '/')
-
-let is_included dir = function
-  | RInclude (dir',_) -> is_prefix (absolute_dir dir') (absolute_dir dir)
-  | Include dir' -> absolute_dir dir = absolute_dir dir'
-  | _ -> false
-
-let dir_of_target t = 
-  match t with
-    | RInclude (dir,_) -> dir
-    | Include dir -> dir
-    | _ -> assert false
-
 let parameters () =
   print "# \n";
   print "# This Makefile may take 3 arguments passed as environment variables:\n";
@@ -237,33 +300,16 @@ let parameters () =
   print "ifndef CAMLP4BIN\n  CAMLP4BIN:=$(CAMLBIN)\nendif\n\n";
   print "CAMLP4LIB:=$(shell $(CAMLP4BIN)$(CAMLP4) -where)\n\n"
 
-let include_dirs l =
-  let rec split_includes l = 
-    match l with
-      | [] -> [], []
-      | Include _ as i :: rem ->
-	  let ri, rr = split_includes rem in 
-	    (i :: ri), rr
-      | RInclude _ as r :: rem -> 
-	  let ri, rr = split_includes rem in 
-	    ri, (r :: rr)
-      | _ :: rem -> split_includes rem
-  in
-  let rec parse_includes l = 
-    match l with
-      | [] -> []
-      | Include x :: rem -> ("-I " ^ x) :: parse_includes rem
-      | RInclude (p,l) :: rem ->
-	  let l' = if l = "" then "\"\"" else l in
-            ("-R " ^ p ^ " " ^ l') :: parse_includes rem
-      | _ :: rem -> parse_includes rem
-  in
-  let l' = if List.exists (is_included ".") l then l else Include "." :: l in
-  let inc_i, inc_r = split_includes l' in
-  let inc_i' = List.filter (fun i -> not (List.exists (fun i' -> is_included (dir_of_target i) i') inc_r)) inc_i in 
+let include_dirs (inc_i,inc_r) =
+  let parse_includes l = List.map (fun (x,_) -> "-I " ^ x) l in
+  let parse_rec_includes l =
+    List.map (fun (p,l,_) ->
+      let l' = if l = "" then "\"\"" else l in "-R " ^ p ^ " " ^ l')
+      l in
+  let inc_i' = List.filter (fun (i,_) -> not (List.exists (fun (i',_,_) -> is_absolute_prefix i' i) inc_r)) inc_i in
   let str_i = parse_includes inc_i in
   let str_i' = parse_includes inc_i' in
-  let str_r = parse_includes inc_r in
+  let str_r = parse_rec_includes inc_r in
     section "Libraries definitions.";
     print "OCAMLLIBS:=-I $(CAMLP4LIB) "; print_list "\\\n  " str_i; print "\n";
     print "COQSRCLIBS:=-I $(COQLIB)/kernel -I $(COQLIB)/lib \\
@@ -295,15 +341,10 @@ let custom sps =
     if sps <> [] then section "Custom targets.";
     List.iter pr_sp sps
 
-let subdirs l =
-  let rec subdirs_aux = function
-    | [] -> []
-    | Subdir x :: r -> x :: (subdirs_aux r)
-    | _ :: r -> subdirs_aux r
-  and pr_subdir s =
+let subdirs sds =
+  let pr_subdir s =
     print s; print ":\n\tcd "; print s; print " ; $(MAKE) all\n\n"
   in
-  let sds = subdirs_aux l in
     if sds <> [] then section "Subdirectories.";
     List.iter pr_subdir sds;
     section "Special targets.";
@@ -311,34 +352,31 @@ let subdirs l =
     print_list " "
       ("all" ::  "opt" :: "byte" :: "archclean" :: "clean" :: "install" 
 	:: "depend" :: "html" :: sds);
-    print "\n\n";
-    sds
-
-let all_target l =
-  let rec parse_arguments l = 
-    match l with
-      | ML n :: r -> let v,m,o = parse_arguments r in (v,n::m,o)
-      | Subdir n :: r -> let v,m,o = parse_arguments r in (v,m,n::o)
-      | V n :: r -> let v,m,o = parse_arguments r in (n::v,m,o)
-      | Special (n,_,_) :: r -> 
-	  let v,m,o = parse_arguments r in 
-	    if is_genrule n then
-	      (v,m,o)
-	    else
-	      (v,m,n::o)
-      | Include _ :: r -> parse_arguments r
-      | RInclude _ :: r -> parse_arguments r
-      | Def _ :: r -> parse_arguments r
-      | [] -> [],[],[]
-  in
-  let 
-      vfiles, mlfiles, other_targets = parse_arguments l
-  in
-    section "Definition of the \"all\" target.";
+    print "\n\n"
+
+let rec split_arguments = function
+  | V n :: r ->
+      let (v,m,o,s),i,d = split_arguments r in ((canonize n::v,m,o,s),i,d)
+  | ML n :: r ->
+      let (v,m,o,s),i,d = split_arguments r in ((v,canonize n::m,o,s),i,d)
+  | Special (n,dep,c) :: r -> 
+      let (v,m,o,s),i,d = split_arguments r in ((v,m,(n,dep,c)::o,s),i,d)
+  | Subdir n :: r ->
+      let (v,m,o,s),i,d = split_arguments r in ((v,m,o,n::s),i,d)
+  | Include p :: r ->
+      let t,(i,r),d = split_arguments r in (t,((p,absolute_dir p)::i,r),d)
+  | RInclude (p,l) :: r ->
+      let t,(i,r),d = split_arguments r in (t,(i,(p,l,absolute_dir p)::r),d)
+  | Def (v,def) :: r -> 
+      let t,i,d = split_arguments r in (t,i,(v,def)::d)
+  | [] -> ([],[],[],[]),([],[]),[]
+
+let main_targets vfiles mlfiles other_targets inc =
     if !some_vfile then
       begin
 	print "VFILES:="; print_list "\\\n  " vfiles; print "\n";
 	print "VOFILES:=$(VFILES:.v=.vo)\n";
+	classify_files_by_root "VOFILES" vfiles inc;
 	print "GLOBFILES:=$(VFILES:.v=.glob)\n";
 	print "VIFILES:=$(VFILES:.v=.vi)\n";
 	print "GFILES:=$(VFILES:.v=.g)\n";
@@ -349,9 +387,11 @@ let all_target l =
       begin
 	print "MLFILES:="; print_list "\\\n  " mlfiles; print "\n";
 	print "CMOFILES:=$(MLFILES:.ml=.cmo)\n";
+	classify_files_by_root "CMOFILES" mlfiles inc;
 	print "CMIFILES:=$(MLFILES:.ml=.cmi)\n";
 	print "CMXFILES:=$(MLFILES:.ml=.cmx)\n";
 	print "CMXSFILES:=$(MLFILES:.ml=.cmxs)\n";
+	classify_files_by_root "CMXSFILES" mlfiles inc;
 	print "OFILES:=$(MLFILES:.ml=.o)\n";
       end;
     print "\nall: ";
@@ -379,6 +419,14 @@ let all_target l =
 	print "\t$(COQDOC) -toc -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $(VFILES)`\n\n";
 	print "\n\n"
       end
+
+let all_target (vfiles, mlfiles, sps, sds) inc =
+  let special_targets = List.filter (fun (n,_,_) -> not (is_genrule n)) sps in
+  let other_targets = List.map (fun x,_,_ -> x) special_targets @ sds in
+  section "Definition of the \"all\" target.";
+  main_targets vfiles mlfiles other_targets inc;
+  custom sps;
+  subdirs sds
       
 let parse f =
   let rec string = parser 
@@ -415,6 +463,8 @@ let rec process_cmd_line = function
       opt := "-opt"; process_cmd_line r
   | "-impredicative-set" :: r ->
       impredicative_set := true; process_cmd_line r
+  | "-no-install" :: r ->
+      no_install := true; process_cmd_line r
   | "-custom" :: com :: dependencies :: file :: r ->
       let check_dep f =
 	if Filename.check_suffix f ".v" then
@@ -498,26 +548,61 @@ let directories_deps l =
   in
     iter ([],[]) l
 
+let ensure_root_dir l =
+  if List.exists (is_included ".") l or not (List.exists has_top_file l) then
+    l
+  else
+    Include "." :: l
+
+let warn_install_at_root_directory (vfiles,mlfiles,_,_) (inc_i,inc_r) =
+  let inc_r_top = List.filter (fun (_,ldir,_) -> ldir = "") inc_r in
+  let inc_top = List.map (fun (p,_,a) -> (p,a)) inc_r_top @ inc_i in
+  let files = vfiles @ mlfiles in
+  if not !no_install &&
+    List.exists (fun f -> List.mem_assoc (Filename.dirname f) inc_top) files
+  then
+    Printf.eprintf "Warning: install target will copy files at the first level of the coq contributions installation directory; option -R %sis recommended\n" 
+      (if inc_r_top = [] then "" else "with non trivial logical root ")
+
+let check_overlapping_include (inc_i,inc_r) =
+  let pwd = Sys.getcwd () in
+  let rec aux = function
+    | [] -> ()
+    | (pdir,_,abspdir)::l ->
+	if not (is_prefix pwd abspdir) then
+	  Printf.eprintf "Warning: in option -R, %s is not a subdirectoty of the current directory\n" pdir;
+	List.iter (fun (pdir',_,abspdir') ->
+	  if is_prefix abspdir abspdir' or is_prefix abspdir' abspdir then
+	    Printf.eprintf "Warning: in options -R, %s and %s overlap\n" pdir pdir') l;
+	List.iter (fun (pdir',abspdir') ->
+	  if is_prefix abspdir abspdir' or is_prefix abspdir' abspdir then
+	    Printf.eprintf "Warning: in option -I, %s overlap with %s in option -R\n" pdir' pdir) inc_i 
+  in aux inc_r
+
 let do_makefile args =
   let l = process_cmd_line args in
-    banner ();
-    header_includes ();
-    warning ();
-    command_line args;
-    parameters ();
-    include_dirs l;
-    variables l;
-    all_target l;
-    let sps = special  l in
-      custom sps;
-      let sds = subdirs l in
-	implicit ();
-	standard sds sps;
-	(* TEST directories_deps l; *)
-	footer_includes ();
-	warning ();
-	if not (!output_channel == stdout) then close_out !output_channel;
-	exit 0
+  let l = ensure_root_dir l in
+  let (_,_,sps,sds as targets), inc, defs = split_arguments l in
+  warn_install_at_root_directory targets inc;
+  check_overlapping_include inc;
+  banner ();
+  header_includes ();
+  warning ();
+  command_line args;
+  parameters ();
+  include_dirs inc;
+  variables defs;
+  all_target targets inc;
+  implicit ();
+  standard ();
+  if not !no_install then install targets inc;
+  clean sds sps;
+  make_makefile sds;
+  (* TEST directories_deps l; *)
+  footer_includes ();
+  warning ();
+  if not (!output_channel == stdout) then close_out !output_channel;
+  exit 0
 	  
 let main () =
   let args =
@@ -527,4 +612,3 @@ let main () =
     do_makefile args
       
 let _ = Printexc.catch main ()
-
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index fec6b0740..9ada5bff2 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -51,7 +51,9 @@ let set_batch_mode () = batch_mode := true
 
 let toplevel_default_name = make_dirpath [id_of_string "Top"]
 let toplevel_name = ref (Some toplevel_default_name)
-let set_toplevel_name dir = toplevel_name := Some dir
+let set_toplevel_name dir =
+  if dir = empty_dirpath then error "Need a non empty toplevel module name";
+  toplevel_name := Some dir
 let unset_toplevel_name () = toplevel_name := None
 
 let remove_top_ml () = Mltop.remove ()
@@ -68,16 +70,16 @@ let outputstate = ref ""
 let set_outputstate s = outputstate:=s
 let outputstate () = if !outputstate <> "" then extern_state !outputstate
 
-let check_coq_overwriting p = 
-  if string_of_id (list_last (repr_dirpath p)) = "Coq" then
-    error "The \"Coq\" logical root directory is reserved for the Coq library"
-
 let set_default_include d = push_include (d,Nameops.default_root_prefix)
 let set_default_rec_include d = push_rec_include(d,Nameops.default_root_prefix)
 let set_include d p =
-  let p = dirpath_of_string p in check_coq_overwriting p; push_include (d,p)
+  let p = dirpath_of_string p in
+  Library.check_coq_overwriting p;
+  push_include (d,p)
 let set_rec_include d p =
-  let p = dirpath_of_string p in check_coq_overwriting p; push_rec_include(d,p)
+  let p = dirpath_of_string p in 
+  Library.check_coq_overwriting p;
+  push_rec_include(d,p)
 
 let load_vernacular_list = ref ([] : (string * bool) list)
 let add_load_vernacular verb s =
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index dcdc46e8e..685eaba3f 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -47,8 +47,10 @@ open Vernacinterp
 
 (* This path is where we look for .cmo *)
 let coq_mlpath_copy = ref ["."]
-let keep_copy_mlpath path = 
-  coq_mlpath_copy := path :: !coq_mlpath_copy
+let keep_copy_mlpath path =
+  let cpath = canonical_path_name path in
+  let filter path' = (cpath <> canonical_path_name path') in
+  coq_mlpath_copy := path :: List.filter filter !coq_mlpath_copy
 
 (* If there is a toplevel under Coq *)
 type toplevel = { 
@@ -106,7 +108,7 @@ let dir_ml_load s =
 	 * if this code section starts to use a module not used elsewhere
 	 * in this file, the Makefile dependency logic needs to be updated.
 	 *)
-        let _,gname = where_in_path true (list_uniquize !coq_mlpath_copy) s in
+        let _,gname = where_in_path true !coq_mlpath_copy s in
         try
           Dynlink.loadfile gname;
 	with | Dynlink.Error a ->
@@ -310,10 +312,10 @@ let cache_ml_module_object (_,{mnames=mnames}) =
 	     if_verbose
 	       msg (str"[Loading ML file " ++ str fname ++ str" ...");
              load_object mname fname;
-             if_verbose msgnl (str"done]");
+             if_verbose msgnl (str" done]");
              add_loaded_module mname
            with e ->
-	     if_verbose msgnl (str"failed]");
+	     if_verbose msgnl (str" failed]");
 	     raise e
 	 else
 	   if_verbose
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index f5603535b..42a06308c 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -182,8 +182,11 @@ let show_match id =
 let print_path_entry (s,l) =
   (str (string_of_dirpath l) ++ str " " ++ tbrk (0,0) ++ str s)
 
-let print_loadpath () =
+let print_loadpath dir =
   let l = Library.get_full_load_paths () in
+  let l = match dir with
+    | None -> l
+    | Some dir -> List.filter (fun (s,l) -> is_dirpath_prefix_of dir l) l in
   msgnl (Pp.t (str "Logical Path:                 " ++
 		 tab () ++ str "Physical path:" ++ fnl () ++
 		 prlist_with_sep pr_fnl print_path_entry l))
@@ -1063,7 +1066,7 @@ let vernac_print = function
   | PrintSectionContext qid -> msg (print_sec_context_typ qid)
   | PrintInspect n -> msg (inspect n)
   | PrintGrammar ent -> Metasyntax.print_grammar ent
-  | PrintLoadPath -> (* For compatibility ? *) print_loadpath ()
+  | PrintLoadPath dir -> (* For compatibility ? *) print_loadpath dir
   | PrintModules -> msg (print_modules ())
   | PrintModule qid -> print_module qid
   | PrintModuleType qid -> print_modtype qid
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 8e797a883..d8084c966 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -38,7 +38,7 @@ type printable =
   | PrintSectionContext of reference
   | PrintInspect of int
   | PrintGrammar of string
-  | PrintLoadPath
+  | PrintLoadPath of dir_path option
   | PrintModules
   | PrintModule of reference
   | PrintModuleType of reference