Imported Upstream version 8.5~beta3+dfsg

18 files changed, 276 insertions, 263 deletions

diff --git a/tools/README.coq-tex b/tools/README.coq-tex
deleted file mode 100755
index 5c7606a9..00000000
--- a/tools/README.coq-tex
+++ /dev/null
@@ -1,13 +0,0 @@
-DESCRIPTION.
-
-The coq-tex filter extracts Coq phrases embedded in LaTeX files,
-evaluates them, and insert the outcome of the evaluation after each
-phrase.
-
-The filter is written in Perl, so you'll need Perl version 4 installed
-on your machine.
-
-USAGE. See the manual page (coq-tex.1).
-
-AUTHOR. Jean-Christophe Filliatre (jcfillia@lip.ens-lyon.fr)
-  from caml-tex of Xavier Leroy.
diff --git a/tools/README.emacs b/tools/README.emacs
index 4d8e3697..4d8e3697 100755..100644
--- a/tools/README.emacs
+++ b/tools/README.emacs
diff --git a/tools/coq-sl.sty b/tools/coq-sl.sty
index 9f6e5480..9f6e5480 100755..100644
--- a/tools/coq-sl.sty
+++ b/tools/coq-sl.sty
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 0931fd55..d3374675 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -299,7 +299,7 @@ let install (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,sds) in
       printf "find %s/%s -maxdepth 0 -and -empty -exec rmdir -p \\{\\} \\;\\n' >> \"$@\"\n" dir kind
     in
     printf "uninstall_me.sh: %s\n" !makefile_name;
-    print "\techo '#!/bin/sh' > $@ \n";
+    print "\techo '#!/bin/sh' > $@\n";
     if (not_empty cmxsfiles) then uninstall_by_root where_what_cmxs;
     uninstall_by_root where_what_oth;
     if not_empty vfiles then uninstall_one_kind "html" doc_dir;
@@ -386,12 +386,12 @@ let implicit () =
     print "$(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib\n\t$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n";
     print "$(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n";
     print "$(addsuffix .d,$(MLLIBFILES)): %.mllib.d: %.mllib\n";
-    print "\t$(COQDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
+    print "\t$(COQDEP) $(OCAMLLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
   let mlpack_rules () =
     print "$(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack\n\t$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^\n\n";
     print "$(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^\n\n";
     print "$(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack\n";
-    print "\t$(COQDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n";
+    print "\t$(COQDEP) $(OCAMLLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n";
 in
   let v_rules () =
     print "$(VOFILES): %.vo: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n";
@@ -496,7 +496,7 @@ endif\n";
           print "\n"
 
 let parameters () =
-  print ".DEFAULT_GOAL := all\n\n# \n";
+  print ".DEFAULT_GOAL := all\n\n";
   print "# This Makefile may take arguments passed as environment variables:\n";
   print "# COQBIN to specify the directory where Coq binaries resides;\n";
   print "# TIMECMD set a command to log .v compilation time;\n";
@@ -575,8 +575,13 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other
   let decl_var var = function
     |[] -> ()
     |l ->
-      printf "%s:=" var; print_list "\\\n  " l; print "\n";
-      printf "\n-include $(addsuffix .d,$(%s))\n.SECONDARY: $(addsuffix .d,$(%s))\n\n" var var
+      printf "%s:=" var; print_list "\\\n  " l; print "\n\n";
+      print "ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),)\n";
+      printf "-include $(addsuffix .d,$(%s))\n" var;
+      print "else\nifeq ($(MAKECMDGOALS),)\n";
+      printf "-include $(addsuffix .d,$(%s))\n" var;
+      print "endif\nendif\n\n";
+      printf ".SECONDARY: $(addsuffix .d,$(%s))\n\n" var
   in
   section "Files dispatching.";
   decl_var "VFILES" vfiles;
@@ -764,7 +769,7 @@ let ensure_root_dir (v,(mli,ml4,ml,mllib,mlpack),_,_) ((ml_inc,i_inc,r_inc) as l
 	&& not_tops mllib && not_tops mlpack) then
     l
   else
-    ((".",here)::ml_inc,(".","Top",here)::i_inc,r_inc)
+    ((".",here)::ml_inc,i_inc,(".","Top",here)::r_inc)
 
 let warn_install_at_root_directory
     (vfiles,(mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles),_,_) (inc_ml,inc_i,inc_r) =
@@ -837,11 +842,9 @@ let do_makefile args =
   if not (makefile = None) then close_out !output_channel;
   exit 0
 
-let main () =
+let _ =
   let args =
     if Array.length Sys.argv = 1 then usage ();
     List.tl (Array.to_list Sys.argv)
   in
     do_makefile args
-
-let _ = Printexc.catch main ()
diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml
index a2cc8384..dbdc2e9d 100644
--- a/tools/coq_tex.ml
+++ b/tools/coq_tex.ml
@@ -24,10 +24,7 @@ let hrule = ref false
 let small = ref false
 let boot = ref false
 
-let coq_prompt = Str.regexp "Coq < "
-let any_prompt = Str.regexp "^[A-Z0-9a-z_\\$']* < "
-
-let remove_prompt s = Str.replace_first any_prompt "" s
+let any_prompt = Str.regexp "[A-Z0-9a-z_\\$']* < "
 
 (* First pass: extract the Coq phrases to evaluate from [texfile]
  * and put them into the file [inputv] *)
@@ -58,30 +55,19 @@ let extract texfile inputv =
       ("Set Printing Width " ^ (string_of_int !linelen) ^".\n");
     outside ()
   with End_of_file ->
-    begin close_in chan_in; close_out chan_out end
+    (* a dummy command, just in case the last line was a comment *)
+    output_string chan_out "Set Printing Width 78.\n";
+    close_in chan_in;
+    close_out chan_out
 
 (* Second pass: insert the answers of Coq from [coq_output] into the
  * TeX file [texfile]. The result goes in file [result]. *)
 
-let begin_coq_example =
-  Str.regexp "\\\\begin{coq_\\(example\\|example\\*\\|example\\#\\)}[ \t]*$"
-let begin_coq_eval = Str.regexp "\\\\begin{coq_eval}[ \t]*$"
-let end_coq_example = Str.regexp "\\\\end{coq_\\(example\\|example\\*\\|example\\#\\)}[ \t]*$"
-let end_coq_eval = Str.regexp "\\\\end{coq_eval}[ \t]*$"
-let dot_end_line = Str.regexp "\\.[ \t]*\\((\\*.*\\*)\\)?[ \t]*$"
-
-let has_match r s =
-  try let _ = Str.search_forward r s 0 in true with Not_found -> false
-
-let percent = Str.regexp "%"
-let bang    = Str.regexp "!"
-let expos   = Str.regexp "^"
-
 let tex_escaped s =
-  let dollar = "\\$" and  backslash = "\\\\" and expon = "\\^" in
-  let delims = Str.regexp ("[_{}&%#" ^ dollar ^ backslash ^ expon ^"~ <>'`]") in
+  let delims = Str.regexp "[_{}&%#$\\^~ <>'`]" in
   let adapt_delim = function
-    | "_" | "{" | "}" | "&" | "%" | "#" | "$" as c -> "\\"^c
+    | "{" | "}" | "&" | "%" | "#" | "$" as c -> "\\"^c
+    | "_" -> "{\\char`\\_}"
     | "\\" -> "{\\char'134}"
     | "^" -> "{\\char'136}"
     | "~" -> "{\\char'176}"
@@ -111,99 +97,106 @@ let insert texfile coq_output result =
   let c_tex = open_in texfile in
   let c_coq = open_in coq_output in
   let c_out = open_out result in
-  (* next_block k : this function reads the next block of Coq output
-   * removing the k leading prompts.
-   * it returns the block as a list of string) *)
-  let last_read = ref "" in
-  let next_block k =
-    if !last_read = "" then last_read := input_line c_coq;
-    (* skip k prompts *)
-    for _i = 1 to k do
-      last_read := remove_prompt !last_read;
-    done;
+  (* read lines until a prompt is found (starting from the second line),
+     purge prompts on the first line and return their number *)
+  let last_read = ref (input_line c_coq) in
+  let read_output () =
+    let first = !last_read in
+    let nb = ref 0 in
+    (* remove the leading prompts *)
+    let rec skip_prompts pos =
+      if Str.string_match any_prompt first pos then
+        let () = incr nb in
+        skip_prompts (Str.match_end ())
+      else pos in
+    let first =
+      let start = skip_prompts 0 in
+      String.sub first start (String.length first - start) in
     (* read and return the following lines until a prompt is found *)
     let rec read_lines () =
       let s = input_line c_coq in
       if Str.string_match any_prompt s 0 then begin
 	last_read := s; []
       end else
-	s :: (read_lines ())
-    in
-    let first = !last_read in first :: (read_lines ())
-  in
-  (* we are just after \end{coq_...} block *)
-  let rec just_after () =
+	s :: read_lines () in
+    (first :: read_lines (), !nb) in
+  let unhandled_output = ref None in
+  let read_output () =
+    match !unhandled_output with
+    | Some some -> unhandled_output := None; some
+    | None -> read_output () in
+  (* we are inside a \begin{coq_...} ... \end{coq_...} block
+   * show_... tell what kind of block it is *)
+  let rec inside show_answers show_questions not_first discarded =
     let s = input_line c_tex in
-    if Str.string_match begin_coq_example s 0 then begin
-      inside (Str.matched_group 1 s <> "example*")
-             (Str.matched_group 1 s <> "example#") 0 false
-    end
-    else begin
-      if !hrule then output_string c_out "\\hrulefill\\\\\n";
-      output_string c_out "\\end{flushleft}\n";
-      if !small then output_string c_out "\\end{small}\n";
-      if Str.string_match begin_coq_eval s 0 then
-	eval 0
+    if s = "" then
+      inside show_answers show_questions not_first (discarded + 1)
+    else if not (Str.string_match end_coq s 0) then begin
+      let (bl,n) = read_output () in
+      assert (n > discarded);
+      let n = n - discarded in
+      if not_first then output_string c_out "\\medskip\n";
+      if !verbose then Printf.printf "Coq < %s\n" s;
+      if show_questions then encapsule false c_out ("Coq < " ^ s);
+      let rec read_lines k =
+        if k = 0 then []
+        else
+          let s = input_line c_tex in
+          if Str.string_match end_coq s 0 then []
+          else s :: read_lines (k - 1) in
+      let al = read_lines (n - 1) in
+      if !verbose then List.iter (Printf.printf "      %s\n") al;
+      if show_questions then
+        List.iter (fun s -> encapsule false c_out ("      " ^ s)) al;
+      let la = n - 1 - List.length al in
+      if la <> 0 then
+        (* this happens when the block ends with a comment; the output
+           is for the command at the beginning of the next block *)
+        unhandled_output := Some (bl, la)
       else begin
-	output_string c_out (s ^ "\n");
-	outside ()
+        if !verbose then List.iter print_endline bl;
+        if show_answers then print_block c_out bl;
+        inside show_answers show_questions (show_answers || show_questions) 0
       end
-    end
+    end else if discarded > 0 then begin
+      (* this happens when the block ends with an empty line *)
+      let (bl,n) = read_output () in
+      assert (n > discarded);
+      unhandled_output := Some (bl, n - discarded)
+    end in
   (* we are outside of a \begin{coq_...} ... \end{coq_...} block *)
-  and outside () =
-    let s = input_line c_tex in
-    if Str.string_match begin_coq_example s 0 then begin
+  let rec outside just_after =
+    let start_block () =
       if !small then output_string c_out "\\begin{small}\n";
       output_string c_out "\\begin{flushleft}\n";
+      if !hrule then output_string c_out "\\hrulefill\\\\\n" in
+    let end_block () =
       if !hrule then output_string c_out "\\hrulefill\\\\\n";
-      inside (Str.matched_group 1 s <> "example*")
-             (Str.matched_group 1 s <> "example#") 0 true
-    end else if Str.string_match begin_coq_eval s 0 then
-      eval 0
-    else begin
-      output_string c_out (s ^ "\n");
-      outside ()
-    end
-  (* we are inside a \begin{coq_example?} ... \end{coq_example?} block
-   * show_answers tells what kind of block it is
-   * k is the number of lines read until now *)
-  and inside show_answers  show_questions k first_block =
+      output_string c_out "\\end{flushleft}\n";
+      if !small then output_string c_out "\\end{small}\n" in
     let s = input_line c_tex in
-    if Str.string_match end_coq_example s 0 then begin
-      just_after ()
+    if Str.string_match begin_coq s 0 then begin
+      let kind = Str.matched_group 1 s in
+      if kind = "eval" then begin
+        if just_after then end_block ();
+        inside false false false 0;
+        outside false
+      end else begin
+        let show_answers   = kind <> "example*" in
+        let show_questions = kind <> "example#" in
+        if not just_after then start_block ();
+        inside show_answers show_questions just_after 0;
+        outside true
+      end
     end else begin
-      let prompt = if k = 0 then "Coq < " else "      " in
-      if !verbose then Printf.printf "%s%s\n" prompt s;
-      if (not first_block) && k=0 then output_string c_out "\\medskip\n";
-      if show_questions then encapsule false c_out (prompt ^ s);
-      if has_match dot_end_line s then begin
-	let bl = next_block (succ k) in
-	if !verbose then List.iter print_endline bl;
-	if show_answers then print_block c_out bl;
-	inside show_answers  show_questions 0 false
-      end else
-	inside show_answers  show_questions (succ k) first_block
-    end
-  (* we are inside a \begin{coq_eval} ... \end{coq_eval} block
-   * k is the number of lines read until now *)
-  and eval k =
-    let s = input_line c_tex in
-    if Str.string_match end_coq_eval s 0 then
-      outside ()
-    else begin
-      if !verbose then Printf.printf "Coq < %s\n" s;
-      if has_match dot_end_line s then
-	let bl = next_block (succ k) in
-	if !verbose then List.iter print_endline bl;
-	eval 0
-      else
-	eval (succ k)
-    end
-  in
+      if just_after then end_block ();
+      output_string c_out (s ^ "\n");
+      outside false
+    end in
   try
-    let _ = next_block 0 in (* to skip the Coq banner *)
-    let _ = next_block 0 in (* to skip the Coq answer to Set Printing Width *)
-    outside ()
+    let _ = read_output () in (* to skip the Coq banner *)
+    let _ = read_output () in (* to skip the Coq answer to Set Printing Width *)
+    outside false
   with End_of_file -> begin
     close_in c_tex;
     close_in c_coq;
@@ -212,7 +205,7 @@ let insert texfile coq_output result =
 
 (* Process of one TeX file *)
 
-let rm f = try Sys.remove f with any -> ()
+let rm f = try Sys.remove f with _ -> ()
 
 let one_file texfile =
   let inputv = Filename.temp_file "coq_tex" ".v" in
@@ -249,7 +242,7 @@ let files = ref []
 let parse_cl () =
   Arg.parse
       [ "-o", Arg.String (fun s -> output_specified := true; output := s),
-	"output-file    Specifiy the resulting LaTeX file";
+	"output-file    Specify the resulting LaTeX file";
 	"-n", Arg.Int (fun n -> linelen := n),
 	"line-width     Set the line width";
 	"-image", Arg.String (fun s -> image := s),
@@ -265,7 +258,7 @@ let parse_cl () =
 	"-small", Arg.Set small,
 	"           Coq parts are written in small font";
 	"-boot", Arg.Set boot,
-	"           Launch coqtop with the -boot option"
+	"            Launch coqtop with the -boot option"
       ]
       (fun s -> files := s :: !files)
       "coq-tex [options] file ..."
@@ -281,7 +274,7 @@ let find_coqtop () =
     "coqtop"
   end
 
-let main () =
+let _ =
   parse_cl ();
   if !image = "" then image := Filename.quote (find_coqtop ());
   if !boot then image := !image ^ " -boot";
@@ -290,9 +283,7 @@ let main () =
     let _ = Sys.command (!image ^ " -batch") in
     exit 1
   end else begin
-    Printf.printf "Your version of coqtop seems OK\n";
+    (*Printf.printf "Your version of coqtop seems OK\n";*)
     flush stdout
   end;
   List.iter one_file (List.rev !files)
-
-let _ = Printexc.catch main ()
diff --git a/tools/coqc.ml b/tools/coqc.ml
index 7e822dbe..e7239da6 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -30,13 +30,8 @@ let verbose = ref false
 let rec make_compilation_args = function
   | [] -> []
   | file :: fl ->
-      let file_noext =
-        if Filename.check_suffix file ".v" then
-          Filename.chop_suffix file ".v"
-        else file
-      in
       (if !verbose then "-compile-verbose" else "-compile")
-      :: file_noext :: (make_compilation_args fl)
+      :: file :: (make_compilation_args fl)
 
 (* compilation of files [files] with command [command] and args [args] *)
 
@@ -109,20 +104,20 @@ let parse_args () =
       |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet"
       |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-beautify"|"-strict-implicit"
       |"-dont-load-proofs"|"-load-proofs"|"-force-load-proofs"
-      |"-impredicative-set"|"-vm"|"-no-native-compiler"
+      |"-impredicative-set"|"-vm"|"-native-compiler"
       |"-verbose-compat-notations"|"-no-compat-notations"
-      |"-indices-matter"|"-quick"|"-color"|"-type-in-type"
+      |"-indices-matter"|"-quick"|"-type-in-type"
       |"-async-proofs-always-delegate"|"-async-proofs-never-reopen-branch"
       as o) :: rem ->
 	parse (cfiles,o::args) rem
 
 (* Options for coqtop : b) options with 1 argument *)
 
-    | ("-outputstate"|"-inputstate"|"-is"|"-exclude-dir"
+    | ("-outputstate"|"-inputstate"|"-is"|"-exclude-dir"|"-color"
       |"-load-vernac-source"|"-l"|"-load-vernac-object"
       |"-load-ml-source"|"-require"|"-load-ml-object"
       |"-init-file"|"-dump-glob"|"-compat"|"-coqlib"|"-top"
-      |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs"
+      |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs" |"-w"
       as o) :: rem ->
 	begin
 	  match rem with
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 2e0cce6e..110d3060 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -36,14 +36,6 @@ let warning_mult suf iter =
   in
   iter check
 
-let add_coqlib_known recur phys_dir log_dir f =
-  match get_extension f [".vo"] with
-    | (basename,".vo") ->
-        let name = log_dir@[basename] in
-	let paths = if recur then suffixes name else [name] in
-        List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths
-    | _ -> ()
-
 let sort () =
   let seen = Hashtbl.create 97 in
   let rec loop file =
@@ -55,13 +47,13 @@ let sort () =
       try
 	while true do
 	  match coq_action lb with
-	    | Require sl ->
+	    | Require (from, sl) ->
 		List.iter
 		  (fun s ->
-		    try loop (Hashtbl.find vKnown s)
-		    with Not_found -> ())
+                    match search_v_known ?from s with
+                    | None -> ()
+                    | Some f -> loop f)
 		sl
-	    | RequireString s -> loop s
 	    | _ -> ()
 	done
       with Fin_fichier ->
@@ -297,18 +289,24 @@ struct
 module DAG = DAG(struct type t = string let compare = compare end)
 
 (** TODO: we should share this code with Coqdep_common *)
+module VData = struct
+  type t = string list option * string list
+  let compare = Pervasives.compare
+end
+
+module VCache = Set.Make(VData)
+
 let treat_coq_file chan =
   let buf = Lexing.from_channel chan in
-  let deja_vu_v = ref ([]: string list list)
-  and deja_vu_ml = ref ([] : string list) in
-  let mark_v_done acc str =
-    let seen = List.mem str !deja_vu_v in
+  let deja_vu_v = ref VCache.empty in
+  let deja_vu_ml = ref StrSet.empty in
+  let mark_v_done from acc str =
+    let seen = VCache.mem (from, str) !deja_vu_v in
     if not seen then
-      let () = addQueue deja_vu_v str in
-      try
-        let file_str = Hashtbl.find vKnown str in
-        (canonize file_str, !suffixe) :: acc
-      with Not_found -> acc
+      let () = deja_vu_v := VCache.add (from, str) !deja_vu_v in
+      match search_v_known ?from str with
+      | None -> acc
+      | Some file_str -> (canonize file_str, !suffixe) :: acc
     else acc
   in
   let rec loop acc =
@@ -317,11 +315,8 @@ let treat_coq_file chan =
     | None -> acc
     | Some action ->
       let acc = match action with
-      | Require strl ->
-        List.fold_left mark_v_done acc strl
-      | RequireString s ->
-        let str = Filename.basename s in
-        mark_v_done acc [str]
+      | Require (from, strl) ->
+        List.fold_left (fun accu v -> mark_v_done from accu v) acc strl
       | Declare sl ->
         let declare suff dir s =
           let base = file_name s dir in
@@ -330,8 +325,8 @@ let treat_coq_file chan =
         in
         let decl acc str =
           let s = basename_noext str in
-          if not (List.mem s !deja_vu_ml) then
-            let () = addQueue deja_vu_ml s in
+          if not (StrSet.mem s !deja_vu_ml) then
+            let () = deja_vu_ml := StrSet.add s !deja_vu_ml in
             match search_mllib_known s with
             | Some mldir -> (declare ".cma" mldir s) :: acc
             | None ->
@@ -343,13 +338,12 @@ let treat_coq_file chan =
         List.fold_left decl acc sl
       | Load str ->
         let str = Filename.basename str in
-        let seen = List.mem [str] !deja_vu_v in
+        let seen = VCache.mem (None, [str]) !deja_vu_v in
         if not seen then
-          let () = addQueue deja_vu_v [str] in
-          try
-            let file_str = Hashtbl.find vKnown [str] in
-            (canonize file_str, ".v") :: acc
-          with Not_found -> acc
+          let () = deja_vu_v := VCache.add (None, [str]) !deja_vu_v in
+          match search_v_known [str] with
+          | None -> acc
+          | Some file_str -> (canonize file_str, ".v") :: acc
         else acc
       | AddLoadPath _ | AddRecLoadPath _ -> acc (** TODO *)
       in
@@ -461,7 +455,7 @@ let rec parse = function
   | "-R" :: ([] | [_]) -> usage ()
   | "-dumpgraph" :: f :: ll -> option_dump := Some (false, f); parse ll
   | "-dumpgraphbox" :: f :: ll -> option_dump := Some (true, f); parse ll
-  | "-exclude-dir" :: r :: ll -> norec_dirnames := r::!norec_dirnames; parse ll
+  | "-exclude-dir" :: r :: ll -> norec_dirnames := StrSet.add r !norec_dirnames; parse ll
   | "-exclude-dir" :: [] -> usage ()
   | "-coqlib" :: r :: ll -> Flags.coqlib_spec := true; Flags.coqlib := r; parse ll
   | "-coqlib" :: [] -> usage ()
diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml
index bc3435a6..64ce66d2 100644
--- a/tools/coqdep_boot.ml
+++ b/tools/coqdep_boot.ml
@@ -25,12 +25,12 @@ let rec parse = function
        (* To solve conflict (e.g. same filename in kernel and checker)
           we allow to state an explicit order *)
        add_caml_dir r;
-       norec_dirs:=r::!norec_dirs;
+       norec_dirs := StrSet.add r !norec_dirs;
        parse ll
   | f :: ll -> treat_file None f; parse ll
   | [] -> ()
 
-let coqdep_boot () =
+let _ =
   let () = option_boot := true in
   if Array.length Sys.argv < 2 then exit 1;
   parse (List.tl (Array.to_list Sys.argv));
@@ -47,5 +47,3 @@ let coqdep_boot () =
   end;
   if !option_c then mL_dependencies ();
   coq_dependencies ()
-
-let _ = Printexc.catch coqdep_boot ()
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index 2e6a15ce..c1111375 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -17,6 +17,11 @@ open Unix
     options (see for instance [option_natdynlk] below).
 *)
 
+module StrSet = Set.Make(String)
+
+module StrList = struct type t = string list let compare = compare end
+module StrListMap = Map.Make(StrList)
+
 let stderr = Pervasives.stderr
 let stdout = Pervasives.stdout
 
@@ -26,8 +31,8 @@ let option_natdynlk = ref true
 let option_boot = ref false
 let option_mldep = ref None
 
-let norec_dirs = ref ([] : string list)
-let norec_dirnames = ref ["CVS"; "_darcs"]
+let norec_dirs = ref StrSet.empty
+let norec_dirnames = ref (List.fold_right StrSet.add ["CVS"; "_darcs"] StrSet.empty)
 
 let suffixe = ref ".vo"
 
@@ -86,18 +91,18 @@ let vAccu   = ref ([] : (string * string) list)
 
 let addQueue q v = q := v :: !q
 
-let safe_hash_add cmp clq q (k,v) =
+let safe_hash_add cmp clq q (k, (v, b)) =
   try
-    let v2 = Hashtbl.find q k in
+    let (v2, _) = Hashtbl.find q k in
     if not (cmp v v2) then
-      let rec add_clash = function
-          (k1,l1)::cltl when k=k1 -> (k1,v::l1)::cltl
-        | cl::cltl -> cl::add_clash cltl
-        | [] -> [(k,[v;v2])] in
-      clq := add_clash !clq;
+      let nv =
+        try v :: StrListMap.find k !clq
+        with Not_found -> [v; v2]
+      in
+      clq := StrListMap.add k nv !clq;
       (* overwrite previous bindings, as coqc does *)
-      Hashtbl.add q k v
-  with Not_found -> Hashtbl.add q k v
+      Hashtbl.add q k (v, b)
+  with Not_found -> Hashtbl.add q k (v, b)
 
 (** Files found in the loadpaths.
     For the ML files, the string is the basename without extension.
@@ -126,20 +131,53 @@ let add_mli_known, iter_mli_known, search_mli_known = mkknown ()
 let add_mllib_known, _, search_mllib_known = mkknown ()
 let add_mlpack_known, _, search_mlpack_known = mkknown ()
 
-let vKnown = (Hashtbl.create 19 : (string list, string) Hashtbl.t)
+let vKnown = (Hashtbl.create 19 : (string list, string * bool) Hashtbl.t)
+(** The associated boolean is true if this is a root path. *)
 let coqlibKnown = (Hashtbl.create 19 : (string list, unit) Hashtbl.t)
 
-let clash_v = ref ([]: (string list * string list) list)
+let get_prefix p l =
+  let rec drop_prefix_rec = function
+    | (h1::tp, h2::tl) when h1 = h2 -> drop_prefix_rec (tp,tl)
+    | ([], tl) -> Some tl
+    | _ -> None
+  in
+  drop_prefix_rec (p, l)
+
+let search_table (type r) is_root table ?from s = match from with
+| None -> Hashtbl.find table s
+| Some from ->
+  let module M = struct exception Found of r end in
+  let iter logpath binding =
+    if is_root binding then match get_prefix from logpath with
+    | None -> ()
+    | Some rem ->
+      match get_prefix (List.rev s) (List.rev rem) with
+      | None -> ()
+      | Some _ -> raise (M.Found binding)
+  in
+  try Hashtbl.iter iter table; raise Not_found
+  with M.Found s -> s
+
+let search_v_known ?from s =
+  let is_root (_, root) = root in
+  try
+    let (phys_dir, _) = search_table is_root vKnown ?from s in
+    Some phys_dir
+  with Not_found -> None
+
+let is_in_coqlib ?from s =
+  let is_root _ = true in
+  try search_table is_root coqlibKnown ?from s; true with Not_found -> false
+
+let clash_v = ref (StrListMap.empty : string list StrListMap.t)
 
 let error_cannot_parse s (i,j) =
   Printf.eprintf "File \"%s\", characters %i-%i: Syntax error\n" s i j;
   exit 1
 
 let warning_module_notfound f s =
-  eprintf "*** Warning: in file %s, library " f;
-  eprintf "%s.v is required and has not been found in the loadpath!\n"
-    (String.concat "." s);
-  flush stderr
+  eprintf "*** Warning: in file %s, library %s is required and has not been found in the loadpath!\n%!"
+    f (String.concat "." s)
 
 let warning_notfound f s =
   eprintf "*** Warning: in file %s, the file " f;
@@ -152,7 +190,7 @@ let warning_declare f s =
   flush stderr
 
 let warning_clash file dir =
-  match List.assoc dir !clash_v with
+  match StrListMap.find dir !clash_v with
     (f1::f2::fl) ->
       let f = Filename.basename f1 in
       let d1 = Filename.dirname f1 in
@@ -165,9 +203,11 @@ let warning_clash file dir =
       eprintf "%s and %s; used the latter)\n" d2 d1
   | _ -> assert false
 
-let safe_assoc verbose file k =
-  if verbose && List.mem_assoc k !clash_v then warning_clash file k;
-  Hashtbl.find vKnown k
+let safe_assoc from verbose file k =
+  if verbose && StrListMap.mem k !clash_v then warning_clash file k;
+  match search_v_known ?from k with
+  | None -> raise Not_found
+  | Some path -> path
 
 let absolute_dir dir =
   let current = Sys.getcwd () in
@@ -222,16 +262,16 @@ let autotraite_fichier_ML md ext =
   try
     let chan = open_in (md ^ ext) in
     let buf = Lexing.from_channel chan in
-    let deja_vu = ref [md] in
+    let deja_vu = ref (StrSet.singleton md) in
     let a_faire = ref "" in
     let a_faire_opt = ref "" in
     begin try
       while true do
 	let (Use_module str) = caml_action buf in
-	if List.mem str !deja_vu then
+	if StrSet.mem str !deja_vu then
 	  ()
 	else begin
-	  addQueue deja_vu str;
+	  deja_vu := StrSet.add str !deja_vu;
 	  let byte,opt = depend_ML str in
 	  a_faire := !a_faire ^ byte;
 	  a_faire_opt := !a_faire_opt ^ opt
@@ -307,38 +347,39 @@ let canonize f =
     | (f,_) :: _ -> escape f
     | _ -> escape f
 
+module VData = struct
+  type t = string list option * string list
+  let compare = Pervasives.compare
+end
+
+module VCache = Set.Make(VData)
+
 let rec traite_fichier_Coq suffixe verbose f =
   try
     let chan = open_in f in
     let buf = Lexing.from_channel chan in
-    let deja_vu_v = ref ([]: string list list)
-    and deja_vu_ml = ref ([] : string list) in
+    let deja_vu_v = ref VCache.empty in
+    let deja_vu_ml = ref StrSet.empty in
     try
       while true do
       	let tok = coq_action buf in
 	match tok with
-	  | Require strl ->
+	  | Require (from, strl) ->
 	      List.iter (fun str ->
-		if not (List.mem str !deja_vu_v) then begin
-	          addQueue deja_vu_v str;
+		if not (VCache.mem (from, str) !deja_vu_v) then begin
+	          deja_vu_v := VCache.add (from, str) !deja_vu_v;
                   try
-                    let file_str = safe_assoc verbose f str in
+                    let file_str = safe_assoc from verbose f str in
                     printf " %s%s" (canonize file_str) suffixe
                   with Not_found ->
-		    if verbose && not (Hashtbl.mem coqlibKnown str) then
+		    if verbose && not (is_in_coqlib ?from str) then
+		      let str =
+			match from with
+			  | None -> str
+			  | Some pth -> pth @ str
+		      in
                       warning_module_notfound f str
        		end) strl
-	  | RequireString s ->
-	      let str = Filename.basename s in
-	      if not (List.mem [str] !deja_vu_v) then begin
-	        addQueue deja_vu_v [str];
-                try
-                  let file_str = Hashtbl.find vKnown [str] in
-                  printf " %s%s" (canonize file_str) suffixe
-                with Not_found ->
-		  if not (Hashtbl.mem coqlibKnown [str]) then
-		    warning_notfound f s
-       	      end
 	  | Declare sl ->
 	      let declare suff dir s =
 		let base = file_name s dir in
@@ -347,8 +388,8 @@ let rec traite_fichier_Coq suffixe verbose f =
 	      in
 	      let decl str =
                 let s = basename_noext str in
-		if not (List.mem s !deja_vu_ml) then begin
-		  addQueue deja_vu_ml s;
+		if not (StrSet.mem s !deja_vu_ml) then begin
+		  deja_vu_ml := StrSet.add s !deja_vu_ml;
 		  match search_mllib_known s with
 		    | Some mldir -> declare ".cma" mldir s
 		    | None ->
@@ -362,10 +403,10 @@ let rec traite_fichier_Coq suffixe verbose f =
 	      in List.iter decl sl
 	  | Load str ->
 	      let str = Filename.basename str in
-	      if not (List.mem [str] !deja_vu_v) then begin
-	        addQueue deja_vu_v [str];
+	      if not (VCache.mem (None, [str]) !deja_vu_v) then begin
+	        deja_vu_v := VCache.add (None, [str]) !deja_vu_v;
                 try
-                  let file_str = Hashtbl.find vKnown [str] in
+                  let (file_str, _) = Hashtbl.find vKnown [str] in
                   let canon = canonize file_str in
                   printf " %s.v" canon;
                   traite_fichier_Coq suffixe true (canon ^ ".v")
@@ -449,14 +490,24 @@ let add_caml_known phys_dir _ f =
     | ".mlpack" -> add_mlpack_known basename (Some phys_dir) suff
     | _ -> ()
 
+let add_coqlib_known recur phys_dir log_dir f =
+  match get_extension f [".vo"] with
+    | (basename,".vo") ->
+        let name = log_dir@[basename] in
+        let paths = if recur then suffixes name else [name] in
+        List.iter (fun f -> Hashtbl.add coqlibKnown f ()) paths
+    | _ -> ()
+
 let add_known recur phys_dir log_dir f =
   match get_extension f [".v";".vo"] with
     | (basename,".v") ->
 	let name = log_dir@[basename] in
 	let file = phys_dir//basename in
-	let paths = if recur then suffixes name else [name] in
-	List.iter
-	  (fun n -> safe_hash_add compare_file clash_v vKnown (n,file)) paths
+	let () = safe_hash_add compare_file clash_v vKnown (name, (file, true)) in
+	if recur then
+          let paths = List.tl (suffixes name) in
+          let iter n = safe_hash_add compare_file clash_v vKnown (n, (file, false)) in
+          List.iter iter paths
     | (basename,".vo") when not(!option_boot) ->
         let name = log_dir@[basename] in
 	let paths = if recur then suffixes name else [name] in
@@ -477,9 +528,9 @@ let rec add_directory recur add_file phys_dir log_dir =
         let phys_f = if phys_dir = "." then f else phys_dir//f in
 	match try (stat phys_f).st_kind with _ -> S_BLK with
 	  | S_DIR when recur ->
-              if List.mem f !norec_dirnames then ()
+              if StrSet.mem f !norec_dirnames then ()
               else
-	        if List.mem phys_f !norec_dirs then ()
+	        if StrSet.mem phys_f !norec_dirs then ()
 	        else
 		  add_directory recur add_file phys_f (log_dir@[f])
 	  | S_REG -> add_file phys_dir log_dir f
diff --git a/tools/coqdep_common.mli b/tools/coqdep_common.mli
index 71b96ca0..d610a055 100644
--- a/tools/coqdep_common.mli
+++ b/tools/coqdep_common.mli
@@ -6,13 +6,15 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+module StrSet : Set.S with type elt = string
+
 val option_c : bool ref
 val option_noglob : bool ref
 val option_boot : bool ref
 val option_natdynlk : bool ref
 val option_mldep : string option ref
-val norec_dirs : string list ref
-val norec_dirnames : string list ref
+val norec_dirs : StrSet.t ref
+val norec_dirnames : StrSet.t ref
 val suffixe : string ref
 type dir = string option
 val ( // ) : string -> string -> string
@@ -31,8 +33,7 @@ val iter_mli_known : (string -> dir -> unit) -> unit
 val search_mli_known : string -> dir option
 val add_mllib_known : string -> dir -> string -> unit
 val search_mllib_known : string -> dir option
-val vKnown : (string list, string) Hashtbl.t
-val coqlibKnown : (string list, unit) Hashtbl.t
+val search_v_known : ?from:string list -> string list -> string option
 val file_name : string -> string option -> string
 val escape : string -> string
 val canonize : string -> string
@@ -40,6 +41,7 @@ val mL_dependencies : unit -> unit
 val coq_dependencies : unit -> unit
 val suffixes : 'a list -> 'a list list
 val add_known : bool -> string -> string list -> string -> unit
+val add_coqlib_known : bool -> string -> string list -> string -> unit
 val add_caml_known : string -> string list -> string -> unit
 val add_directory :
   bool ->
diff --git a/tools/coqdep_lexer.mli b/tools/coqdep_lexer.mli
index b447030a..84c9ba79 100644
--- a/tools/coqdep_lexer.mli
+++ b/tools/coqdep_lexer.mli
@@ -11,8 +11,7 @@ type mL_token = Use_module of string
 type qualid = string list
 
 type coq_token =
-    Require of qualid list
-  | RequireString of string
+    Require of qualid option * qualid list
   | Declare of string list
   | Load of string
   | AddLoadPath of string
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll
index 8ecc419c..291bc55f 100644
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.mll
@@ -16,8 +16,7 @@
   type qualid = string list
 
   type coq_token =
-    | Require of qualid list
-    | RequireString of string
+    | Require of qualid option * qualid list
     | Declare of string list
     | Load of string
     | AddLoadPath of string
@@ -271,16 +270,9 @@ and require_file = parse
         module_names := [coq_qual_id_tail lexbuf];
         let qid = coq_qual_id_list lexbuf in
         parse_dot lexbuf;
-	match !from_pre_ident with
-	  None ->
-          Require qid
-	| Some from ->
-	  (from_pre_ident := None ;
-	   Require (List.map (fun x -> from @ x) qid)) }
-  | '"' [^'"']* '"' (*'"'*)
-      { let s = Lexing.lexeme lexbuf in
-        parse_dot lexbuf;
-        RequireString (unquote_vfile_string s) }
+        let from = !from_pre_ident in
+        from_pre_ident := None;
+        Require (from, qid) }
   | eof
       { syntax_error lexbuf }
   | _
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index cb704146..d2892167 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -320,6 +320,7 @@ let def_token =
   | "Instance"
   | "Declare" space+ "Instance"
   | "Global" space+ "Instance"
+  | "Functional" space+ "Scheme"
 
 let decl_token =
   "Hypothesis"
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 9531cd2b..22febd6a 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -61,8 +61,8 @@ let usage () =
   prerr_endline "  --coqlib_path <dir>  set the path where Coq files are installed";
   prerr_endline "  -R <dir> <coqdir>    map physical dir to Coq dir";
   prerr_endline "  -Q <dir> <coqdir>    map physical dir to Coq dir";
-  prerr_endline "  --latin1             set ISO-8859-1 input language";
-  prerr_endline "  --utf8               set UTF-8 input language";
+  prerr_endline "  --latin1             set ISO-8859-1 mode";
+  prerr_endline "  --utf8               set UTF-8 mode";
   prerr_endline "  --charset <string>   set HTML charset";
   prerr_endline "  --inputenc <string>  set LaTeX input encoding";
   prerr_endline "  --interpolate        try to typeset identifiers in comments using definitions in the same module";
@@ -557,10 +557,8 @@ let produce_output fl =
 (*s \textbf{Main program.} Print the banner, parse the command line,
     read the files and then call [produce_document] from module [Web]. *)
 
-let main () =
+let _ =
   let files = parse () in
     Index.init_coqlib_library ();
     if not !quiet then banner ();
     if files <> [] then produce_output files
-
-let _ = Printexc.catch main ()
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 06030c45..8589f94a 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -197,8 +197,11 @@ module Latex = struct
     printf "\n";
     printf "%%Warning: tipa declares many non-standard macros used by utf8x to\n";
     printf "%%interpret utf8 characters but extra packages might have to be added\n";
-    printf "%%(e.g. \"textgreek\" for Greek letters not already in tipa).\n";
-    printf "%%Use coqdoc's option -p to add new packages.\n";
+    printf "%%such as \"textgreek\" for Greek letters not already in tipa\n";
+    printf "%%or \"stmaryrd\" for mathematical symbols.\n";
+    printf "%%Utf8 codes missing a LaTeX interpretation can be defined by using\n";
+    printf "%%\\DeclareUnicodeCharacter{code}{interpretation}.\n";
+    printf "%%Use coqdoc's option -p to add new packages or declarations.\n";
     printf "\\usepackage{tipa}\n";
     printf "\n"
 
diff --git a/tools/coqwc.mll b/tools/coqwc.mll
index 417ec535..9a42553d 100644
--- a/tools/coqwc.mll
+++ b/tools/coqwc.mll
@@ -276,7 +276,7 @@ let rec parse = function
 
 (*s Main program. *)
 
-let main () =
+let _ =
   let files = parse (List.tl (Array.to_list Sys.argv)) in
   if not (!spec_only || !proof_only) then
     printf "     spec    proof comments\n";
@@ -285,8 +285,6 @@ let main () =
     | [f] -> process_file f
     | _ -> List.iter process_file files; print_totals ()
 
-let _ = Printexc.catch main ()
-
 (*i*)}(*i*)
 
 
diff --git a/tools/fake_ide.ml b/tools/fake_ide.ml
index c2b12668..a9a7251c 100644
--- a/tools/fake_ide.ml
+++ b/tools/fake_ide.ml
@@ -90,7 +90,7 @@ module Parser = struct (* {{{ *)
       in find ~-1 0
     else raise (Err ("Balanced "^String.make 1 c^" not found in: "^s))
 
-  let eat_blanks s = snd (eat_rex "[ \n\t]*") s
+  let eat_blanks s = snd (eat_rex "[ \r\n\t]*") s
 
   let s = ref ""
 
@@ -257,6 +257,9 @@ let eval_print l coq =
   | [ Tok(_,"WAIT") ] ->
       let phrase = "Stm Wait." in
       eval_call (query (phrase,tip_id())) coq
+  | [ Tok(_,"JOIN") ] ->
+      let phrase = "Stm JoinDocument." in
+      eval_call (query (phrase,tip_id())) coq
   | [ Tok(_,"ASSERT"); Tok(_,"TIP"); Tok(_,id) ] ->
       let to_id, _ = get_id id in
       if not(Stateid.equal (Document.tip doc) to_id) then error "Wrong tip"
@@ -273,6 +276,7 @@ let grammar =
     ; Seq [Item (eat_rex "EDIT_AT"); Item eat_id]
     ; Seq [Item (eat_rex "QUERY"); Opt (Item eat_id); Item eat_phrase]
     ; Seq [Item (eat_rex "WAIT")]
+    ; Seq [Item (eat_rex "JOIN")]
     ; Seq [Item (eat_rex "GOALS")]
     ; Seq [Item (eat_rex "FAILGOALS")]
     ; Seq [Item (eat_rex "ASSERT"); Item (eat_rex "TIP"); Item eat_id ]
diff --git a/tools/gallina.ml b/tools/gallina.ml
index 279919c5..5ce19e7f 100644
--- a/tools/gallina.ml
+++ b/tools/gallina.ml
@@ -39,7 +39,7 @@ let traite_stdin () =
   with Sys_error _ ->
     ()
 
-let gallina () =
+let _ =
   let lg_command = Array.length Sys.argv in
   if lg_command < 2 then begin
     output_string stderr "Usage: gallina [-] [-stdout] file1 file2 ...\n";
@@ -59,6 +59,3 @@ let gallina () =
     traite_stdin ()
   else
     List.iter traite_fichier !vfiles
-
-let _ = Printexc.catch gallina ()
-