Imported Upstream version 8.5~beta1+dfsg

14 files changed, 183 insertions, 135 deletions

diff --git a/tools/coqdoc/alpha.ml b/tools/coqdoc/alpha.ml
index 6a44684d..c3db3a26 100644
--- a/tools/coqdoc/alpha.ml
+++ b/tools/coqdoc/alpha.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/coqdoc/alpha.mli b/tools/coqdoc/alpha.mli
index 9d3593ea..46005741 100644
--- a/tools/coqdoc/alpha.mli
+++ b/tools/coqdoc/alpha.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index 443edc0b..de7290a4 100644
--- a/tools/coqdoc/cdglobals.ml
+++ b/tools/coqdoc/cdglobals.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -25,12 +25,14 @@ let out_to = ref MultFiles
 
 let out_channel = ref stdout
 
+let ( / ) = Filename.concat
+
 let coqdoc_out f =
   if !output_dir <> "" && Filename.is_relative f then
     if not (Sys.file_exists !output_dir) then
       (Printf.eprintf "No such directory: %s\n" !output_dir; exit 1)
     else
-      Filename.concat !output_dir f
+      !output_dir / f
   else
     f
 
@@ -71,17 +73,19 @@ let normalize_filename f =
 (** A weaker analog of the function in Envars *)
 
 let guess_coqlib () =
-  let file = "states/initial.coq" in
+  let file = "theories/Init/Prelude.vo" in
   match Coq_config.coqlib with
-    | Some coqlib when Sys.file_exists (Filename.concat coqlib file) ->
-      coqlib
+    | Some coqlib when Sys.file_exists (coqlib / file) -> coqlib
     | Some _ | None ->
       let coqbin = normalize_path (Filename.dirname Sys.executable_name) in
       let prefix = Filename.dirname coqbin in
-      let rpath = if Coq_config.local then [] else
-	  (if Coq_config.arch = "win32" then ["lib"] else ["lib";"coq"]) in
-      let coqlib = List.fold_left Filename.concat prefix rpath in
-      if Sys.file_exists (Filename.concat coqlib file) then coqlib
+      let rpath =
+        if Coq_config.local then []
+        else if Coq_config.arch_is_win32 then ["lib"]
+        else ["lib/coq"]
+      in
+      let coqlib = List.fold_left (/) prefix rpath in
+      if Sys.file_exists (coqlib / file) then coqlib
       else prefix
 
 let header_trailer = ref true
diff --git a/tools/coqdoc/coqdoc.css b/tools/coqdoc/coqdoc.css
index ccd285f1..dbc930f5 100644
--- a/tools/coqdoc/coqdoc.css
+++ b/tools/coqdoc/coqdoc.css
@@ -75,7 +75,7 @@ h4.section {
                    padding-top: 0px; 
                    padding-bottom: 0px; 
                    font-size : 100%;
-                   font-style : bold;
+                   font-weight : bold;
                    text-decoration : underline;
  }
 
@@ -86,8 +86,7 @@ h4.section {
              max-width: 40em;
              color: black;
 	     padding: 10px;
-             background-color: #90bdff;
-             border-style: plain}
+             background-color: #90bdff }
 
 .inlinecode { 
     display: inline;
@@ -160,8 +159,65 @@ tr.infrulemiddle hr {
 #footer { font-size: 65%;
           font-family: sans-serif; }
 
+/* Identifiers: <span class="id" title="...">) */
+
 .id { display: inline; }
 
+.id[title="constructor"] {
+    color: rgb(60%,0%,0%);
+}
+
+.id[title="var"] {
+    color: rgb(40%,0%,40%);
+}
+
+.id[title="variable"] {
+    color: rgb(40%,0%,40%);
+}
+
+.id[title="definition"] {
+    color: rgb(0%,40%,0%);
+}
+
+.id[title="abbreviation"] {
+    color: rgb(0%,40%,0%);
+}
+
+.id[title="lemma"] {
+    color: rgb(0%,40%,0%);
+}
+
+.id[title="instance"] {
+    color: rgb(0%,40%,0%);
+}
+
+.id[title="projection"] {
+    color: rgb(0%,40%,0%);
+}
+
+.id[title="method"] {
+    color: rgb(0%,40%,0%);
+}
+
+.id[title="inductive"] {
+    color: rgb(0%,0%,80%);
+}
+
+.id[title="record"] {
+    color: rgb(0%,0%,80%);
+}
+
+.id[title="class"] {
+    color: rgb(0%,0%,80%);
+}
+
+.id[title="keyword"] {
+ color : #cf1d1d;
+/*     color: black; */
+}
+
+/* Deprecated rules using the 'type' attribute of <span> (not xhtml valid) */
+
 .id[type="constructor"] { 
     color: rgb(60%,0%,0%);
 }
@@ -261,7 +317,6 @@ tr.infrulemiddle hr {
 #index #footer {
     position: absolute;
     bottom: 0;
-    text-align: bottom;
 }
 
 .paragraph {
diff --git a/tools/coqdoc/coqdoc.sty b/tools/coqdoc/coqdoc.sty
index 9de9a38f..f49f9f00 100644
--- a/tools/coqdoc/coqdoc.sty
+++ b/tools/coqdoc/coqdoc.sty
@@ -1,5 +1,5 @@
 
-% This is coqdoc.sty, by Jean-Christophe Filliâtre
+% This is coqdoc.sty, by Jean-Christophe Filliâtre
 % This LaTeX package is used by coqdoc (http://www.lri.fr/~filliatr/coqdoc)
 %
 % You can modify the following macros to customize the appearance
diff --git a/tools/coqdoc/cpretty.mli b/tools/coqdoc/cpretty.mli
index 390e61d2..4e132ba0 100644
--- a/tools/coqdoc/cpretty.mli
+++ b/tools/coqdoc/cpretty.mli
@@ -1,12 +1,10 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Index
-
 val coq_file : string -> Cdglobals.coq_module -> unit
 val detect_subtitle : string -> Cdglobals.coq_module -> string option
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 300d104c..edf7ee8e 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -12,13 +12,6 @@
   open Printf
   open Lexing
 
-  (* A function that emulates Lexing.new_line (which does not exist in OCaml < 3.11.0) *)
-  let new_line lexbuf =
-    let pos = lexbuf.lex_curr_p in
-      lexbuf.lex_curr_p <- { pos with
-	pos_lnum = pos.pos_lnum + 1;
-	pos_bol = pos.pos_cnum }
-
   (* A list function we need *)
   let rec take n ls =
     if n = 0 then [] else
@@ -75,7 +68,6 @@
   let brackets = ref 0
   let comment_level = ref 0
   let in_proof = ref None
-  let in_emph = ref false
 
   let in_env start stop = 
     let r = ref false in
@@ -102,8 +94,6 @@
             let length_skip = 1 + String.length s1 in
               lexbuf.lex_curr_pos <- lexbuf.lex_start_pos + length_skip
 
-  let is_space = function ' ' | '\t' | '\n' | '\r' -> true | _ -> false
-
   (* saving/restoring the PP state *)
 
   type state = {
@@ -127,8 +117,6 @@
 
   let without_light = without_ref Cdglobals.light
 
-  let show_all f = without_gallina (without_light f)
-
   let begin_show () = save_state (); Cdglobals.gallina := false; Cdglobals.light := false
   let end_show () = restore_state ()
 
@@ -251,14 +239,6 @@
     with _ ->
       ()
 
-  let extract_ident_re = Str.regexp "([ \t]*\\([^ \t]+\\)[ \t]*:="
-  let extract_ident s =
-    assert (String.length s >= 3);
-    if Str.string_match extract_ident_re s 0 then
-      Str.matched_group 1 s
-    else
-      String.sub s 1 (String.length s - 3)
-
   let output_indented_keyword s lexbuf =
     let nbsp,isp = count_spaces s in
     Output.indentation nbsp;
@@ -282,10 +262,8 @@ let firstchar =
   '\195' ['\152'-'\182'] |
   '\195' ['\184'-'\191'] |
   (* utf-8 letterlike symbols *)
-  (* '\206' ([ '\145' - '\183'] | '\187') | *)
-  (* '\xCF' [ '\x00' - '\xCE' ] |  *)
-  (* utf-8 letterlike symbols *)
-  '\206' (['\145'-'\161'] | ['\163'-'\187']) |
+  '\206' (['\145'-'\161'] | ['\163'-'\191']) |
+  '\207' (['\145'-'\191']) |
   '\226' ('\130' [ '\128'-'\137' ] (* subscripts *)
     | '\129' [ '\176'-'\187' ] (* superscripts *)
     | '\132' ['\128'-'\191'] | '\133' ['\128'-'\143'])
@@ -333,6 +311,7 @@ let def_token =
   | "Boxed"
   | "CoFixpoint"
   | "Record"
+  | "Variant"
   | "Structure"
   | "Scheme"
   | "Inductive"
@@ -345,7 +324,7 @@ let def_token =
 let decl_token =
   "Hypothesis"
   | "Hypotheses"
-  | "Parameter"
+  | "Parameter" 's'?
   | "Axiom" 's'?
   | "Conjecture"
 
@@ -626,7 +605,7 @@ and coq = parse
 	    end
 	  else
 	    begin
-	      Output.ident s (lexeme_start lexbuf);
+	      Output.ident s None;
 	      let eol=body lexbuf in
 		if eol then coq_bol lexbuf else coq lexbuf
 	    end }
@@ -656,17 +635,17 @@ and coq = parse
 	if eol then coq_bol lexbuf else coq lexbuf }
   | gallina_kw
       { let s = lexeme lexbuf in
-	  Output.ident s (lexeme_start lexbuf);
+	  Output.ident s None;
 	let eol = body lexbuf in
 	  if eol then coq_bol lexbuf else coq lexbuf }
   | notation_kw
       { let s = lexeme lexbuf in
-	Output.ident s (lexeme_start lexbuf);
+	Output.ident s None;
 	let eol= start_notation_string lexbuf in
 	if eol then coq_bol lexbuf else coq lexbuf }
   | prog_kw
       { let s = lexeme lexbuf in
-	  Output.ident s (lexeme_start lexbuf);
+	  Output.ident s None;
 	let eol = body lexbuf in
 	  if eol then coq_bol lexbuf else coq lexbuf }
   | space+ { Output.char ' '; coq lexbuf }
@@ -914,11 +893,15 @@ and doc indents = parse
 and escaped_math_latex = parse
   | "$" { Output.stop_latex_math () }
   | eof { Output.stop_latex_math () }
+  | "*)"
+        { Output.stop_latex_math (); backtrack lexbuf }
   | _   { Output.latex_char (lexeme_char lexbuf 0); escaped_math_latex lexbuf }
 
 and escaped_latex = parse
   | "%" { () }
   | eof { () }
+  | "*)"
+        { backtrack lexbuf }
   | _   { Output.latex_char (lexeme_char lexbuf 0); escaped_latex lexbuf }
 
 and escaped_html = parse
@@ -928,12 +911,15 @@ and escaped_html = parse
   | "##"
         { Output.html_char '#'; escaped_html lexbuf }
   | eof { () }
+  | "*)"
+        { backtrack lexbuf }
   | _   { Output.html_char (lexeme_char lexbuf 0); escaped_html lexbuf }
 
 and verbatim inline = parse
   | nl ">>" space* nl { Output.verbatim_char inline '\n'; Output.stop_verbatim inline }
   | nl ">>" { Output.verbatim_char inline '\n'; Output.stop_verbatim inline }
   | ">>" { Output.stop_verbatim inline }
+  | "*)" { Output.stop_verbatim inline; backtrack lexbuf }
   | eof { Output.stop_verbatim inline }
   | _ { Output.verbatim_char inline (lexeme_char lexbuf 0); verbatim inline lexbuf }
 
@@ -953,11 +939,11 @@ and escaped_coq = parse
   | "]"
       { decr brackets;
 	if !brackets > 0 then
-	  (Output.sublexer ']' (lexeme_start lexbuf); escaped_coq lexbuf)
+	  (Output.sublexer_in_doc ']'; escaped_coq lexbuf)
 	else Tokens.flush_sublexer () }
   | "["
       { incr brackets;
-        Output.sublexer '[' (lexeme_start lexbuf); escaped_coq lexbuf }
+        Output.sublexer_in_doc '['; escaped_coq lexbuf }
   | "(*"
       { Tokens.flush_sublexer (); comment_level := 1;
         ignore (comment lexbuf); escaped_coq lexbuf }
@@ -967,7 +953,7 @@ and escaped_coq = parse
       { Tokens.flush_sublexer () }
   | (identifier '.')* identifier
       { Tokens.flush_sublexer();
-        Output.ident (lexeme lexbuf) (lexeme_start lexbuf);
+        Output.ident (lexeme lexbuf) None;
         escaped_coq lexbuf }
   | space_nl*
       { let str = lexeme lexbuf in
@@ -979,7 +965,7 @@ and escaped_coq = parse
                                         else Output.start_inline_coq ());
           escaped_coq lexbuf }
   | _ 
-      { Output.sublexer (lexeme_char lexbuf 0) (lexeme_start lexbuf);
+      { Output.sublexer_in_doc (lexeme_char lexbuf 0);
         escaped_coq lexbuf }
 
 (*s Coq "Comments" command. *)
@@ -1078,7 +1064,7 @@ and body_bol = parse
   | _ { backtrack lexbuf; Output.indentation 0; body lexbuf }
 
 and body = parse
-  | nl {Tokens.flush_sublexer(); Output.line_break(); new_line lexbuf; body_bol lexbuf}
+  | nl {Tokens.flush_sublexer(); Output.line_break(); Lexing.new_line lexbuf; body_bol lexbuf}
   | nl+ space* "]]" space* nl
       { Tokens.flush_sublexer();
         if not !formatted then
@@ -1147,11 +1133,11 @@ and body = parse
 	     else body lexbuf }
   | "where" 
       { Tokens.flush_sublexer();
-        Output.ident (lexeme lexbuf) (lexeme_start lexbuf);
+        Output.ident (lexeme lexbuf) None;
 	start_notation_string lexbuf }
   | identifier
       { Tokens.flush_sublexer();
-        Output.ident (lexeme lexbuf) (lexeme_start lexbuf);
+        Output.ident (lexeme lexbuf) (Some (lexeme_start lexbuf));
 	body lexbuf }
   | ".."
       { Tokens.flush_sublexer(); Output.char '.'; Output.char '.';
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index 8170e173..4a5ff592 100644
--- a/tools/coqdoc/index.ml
+++ b/tools/coqdoc/index.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Filename
-open Lexing
 open Printf
 open Cdglobals
 
@@ -36,7 +34,6 @@ type index_entry =
   | Def of string * entry_type
   | Ref of coq_module * string * entry_type
 
-let current_type : entry_type ref = ref Library
 let current_library = ref ""
   (** refers to the file being parsed *)
 
@@ -95,9 +92,6 @@ let empty_stack = []
 let module_stack = ref empty_stack
 let section_stack = ref empty_stack
 
-let init_stack () =
-  module_stack := empty_stack; section_stack := empty_stack
-
 let push st p = st := p::!st
 let pop st =
   match !st with
@@ -109,27 +103,6 @@ let head st =
     | [] -> ""
     | x::_ -> x
 
-let begin_module m = push module_stack m
-let begin_section s = push section_stack s
-
-let end_block id =
-  (** determines if it ends a module or a section and pops the stack *)
-  if ((String.compare (head !module_stack) id ) == 0) then
-    pop module_stack
-  else if ((String.compare (head !section_stack) id) == 0) then
-    pop section_stack
-  else
-    ()
-
-let make_fullid id =
-  (** prepends the current module path to an id *)
-  let path = string_of_stack !module_stack in
-    if String.length path > 0 then
-      path ^ "." ^ id
-    else
-      id
-
-
 (* Coq modules *)
 
 let split_sp s =
@@ -158,7 +131,7 @@ let find_external_library logicalpath =
   let rec aux = function
     | [] -> raise Not_found
     | (l,u)::rest ->
-        if String.length logicalpath > String.length l &
+        if String.length logicalpath > String.length l &&
           String.sub logicalpath 0 (String.length l + 1) = l ^"."
         then u
         else aux rest
@@ -208,10 +181,6 @@ let sort_entries el =
 
 let display_letter c = if c = '*' then "other" else String.make 1 c
 
-let index_size = List.fold_left (fun s (_,l) -> s + List.length l) 0
-
-let hashtbl_elements h = Hashtbl.fold (fun x y l -> (x,y)::l) h []
-
 let type_name = function
   | Library ->
       let ln = !lib_name in
@@ -304,9 +273,9 @@ let type_of_string = function
   | "def" | "coe" | "subclass" | "canonstruc" | "fix" | "cofix"
   | "ex" | "scheme" -> Definition
   | "prf" | "thm" -> Lemma
-  | "ind" | "coind" -> Inductive
+  | "ind" | "variant" | "coind" -> Inductive
   | "constr" -> Constructor
-  | "rec" | "corec" -> Record
+  | "indrec" | "rec" | "corec" -> Record
   | "proj" -> Projection
   | "class" -> Class
   | "meth" -> Method
@@ -319,7 +288,7 @@ let type_of_string = function
   | "mod" | "modtype" -> Module
   | "tac" -> TacticDefinition
   | "sec" -> Section
-  | s -> raise (Invalid_argument ("type_of_string:" ^ s))
+  | s -> invalid_arg ("type_of_string:" ^ s)
 
 let ill_formed_glob_file f =
   eprintf "Warning: ill-formed file %s (links will not be available)\n" f
@@ -370,9 +339,6 @@ let read_glob vfile f =
 		    done)
 	       with _ -> ())
 	  | _ ->
-	      try Scanf.sscanf s "not %d %s %s"
-		(fun loc sp id -> add_def loc loc (type_of_string "not") sp id)
-	      with Scanf.Scan_failure _ ->
 	      try Scanf.sscanf s "%s %d:%d %s %s"
 		(fun ty loc1 loc2 sp id ->
                   add_def loc1 loc2 (type_of_string ty) sp id)
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli
index 4c1a445c..69b4e4da 100644
--- a/tools/coqdoc/index.mli
+++ b/tools/coqdoc/index.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 59d1ac87..9531cd2b 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -60,6 +60,7 @@ let usage () =
   prerr_endline "  --boot               run in boot mode";
   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 "  --charset <string>   set HTML charset";
@@ -320,6 +321,10 @@ let parse () =
 	add_path path log; parse_rec rem
     | "-R" :: ([] | [_]) ->
 	usage ()
+    | "-Q" :: path :: log :: rem ->
+	add_path path log; parse_rec rem
+    | "-Q" :: ([] | [_]) ->
+	usage ()
     | ("-glob-from" | "--glob-from") :: f :: rem ->
 	glob_source := GlobFile f; parse_rec rem
     | ("-glob-from" | "--glob-from") :: [] ->
@@ -445,7 +450,7 @@ let gen_mult_files l =
       if (!header_trailer) then Output.trailer ();
       close_out_file()
     end
-      (* Rq: pour latex et texmacs, une toc ou un index séparé n'a pas de sens... *)
+    (* NB: for latex and texmacs, a separated toc or index is meaningless... *)
 
 let read_glob_file vfile f =
   try Index.read_glob vfile f
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 2d29c447..ae6e6388 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -41,7 +41,7 @@ let is_keyword =
       "Mutual"; "Parameter"; "Parameters"; "Print"; "Printing"; "All"; "Proof"; "Proof with"; "Qed";
       "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme"; "Assumptions"; "Axioms"; "Universes";
       "Induction"; "for"; "Sort"; "Section"; "Show"; "Structure"; "Syntactic"; "Syntax"; "Tactic"; "Theorem";
-      "Search"; "SearchAbout"; "SearchRewrite";
+      "Search"; "SearchAbout"; "SearchHead"; "SearchPattern"; "SearchRewrite";
       "Set"; "Types"; "Undo"; "Unset"; "Variable"; "Variables"; "Context";
       "Notation"; "Reserved Notation"; "Tactic Notation";
       "Delimit"; "Bind"; "Open"; "Scope"; "Inline";
@@ -50,6 +50,7 @@ let is_keyword =
       "subgoal"; "subgoals"; "vm_compute";
       "Opaque"; "Transparent"; "Time";
       "Extraction"; "Extract";
+      "Variant";
       (* Program *)
       "Program Definition"; "Program Example"; "Program Fixpoint"; "Program Lemma";
       "Obligation"; "Obligations"; "Solve"; "using"; "Next Obligation"; "Next";
@@ -59,7 +60,7 @@ let is_keyword =
       "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; "where"; "struct"; "wf"; "measure";
       "fix"; "cofix";
       (* Ltac *)
-      "before"; "after"; "constr"; "ltac"; "goal"; "context"; "beta"; "delta"; "iota"; "zeta";
+      "before"; "after"; "constr"; "ltac"; "goal"; "context"; "beta"; "delta"; "iota"; "zeta"; "lazymatch";
       (* Notations *)
       "level"; "associativity"; "no"
        ]
@@ -210,6 +211,7 @@ module Latex = struct
       printf "\\usepackage{fullpage}\n";
       printf "\\usepackage{coqdoc}\n";
       printf "\\usepackage{amsmath,amssymb}\n";
+      printf "\\usepackage{url}\n";
       (match !toc_depth with
        | None -> ()
        | Some n -> printf "\\setcounter{tocdepth}{%i}\n" n);
@@ -383,6 +385,14 @@ module Latex = struct
     end;
     last_was_in := false
 
+  let sublexer_in_doc c =
+    if c = '*' && !last_was_in then begin
+      Tokens.flush_sublexer ();
+      output_char '*'
+    end else
+      Tokens.output_tagged_symbol_char None c;
+    last_was_in := false
+
   let initialize () =
     initialize_tex_html ();
     Tokens.token_tree := token_tree_latex;
@@ -399,8 +409,11 @@ module Latex = struct
   let ident s loc =
     last_was_in := s = "in";
     try
-      let tag = Index.find (get_module false) loc in
-      reference (translate s) tag
+      match loc with
+      | None -> raise Not_found
+      | Some loc ->
+          let tag = Index.find (get_module false) loc in
+          reference (translate s) tag
     with Not_found ->
       if is_tactic s then
 	printf "\\coqdoctac{%s}" (translate s)
@@ -522,8 +535,8 @@ module Html = struct
 	  printf "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Strict//EN\"\n";
 	  printf "\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd\">\n";
 	  printf "<html xmlns=\"http://www.w3.org/1999/xhtml\">\n<head>\n";
-	  printf "<meta http-equiv=\"Content-Type\" content=\"text/html; charset=%s\"/>\n" !charset;
-	  printf "<link href=\"coqdoc.css\" rel=\"stylesheet\" type=\"text/css\"/>\n";
+	  printf "<meta http-equiv=\"Content-Type\" content=\"text/html; charset=%s\" />\n" !charset;
+	  printf "<link href=\"coqdoc.css\" rel=\"stylesheet\" type=\"text/css\" />\n";
 	  printf "<title>%s</title>\n</head>\n\n" !page_title;
 	  printf "<body>\n\n<div id=\"page\">\n\n<div id=\"header\">\n</div>\n\n";
 	  printf "<div id=\"main\">\n\n"
@@ -558,7 +571,7 @@ module Html = struct
           printf "<h1 class=\"libtitle\">%s %s</h1>\n\n" ln (get_module true)
     end
 
-  let indentation n = for i = 1 to n do printf "&nbsp;" done
+  let indentation n = for _i = 1 to n do printf "&nbsp;" done
 
   let line_break () = printf "<br/>\n"
 
@@ -573,9 +586,6 @@ module Html = struct
     | '&' -> printf "&amp;"
     | c -> output_char c
 
-  let raw_string s =
-    for i = 0 to String.length s - 1 do char s.[i] done
-
   let escaped =
     let buff = Buffer.create 5 in
     fun s ->
@@ -585,10 +595,24 @@ module Html = struct
 	| '<' -> Buffer.add_string buff "&lt;"
 	| '>' -> Buffer.add_string buff "&gt;"
 	| '&' -> Buffer.add_string buff "&amp;"
+        | '\'' -> Buffer.add_string buff "&acute;"
+        | '\"' -> Buffer.add_string buff "&quot;"
 	| c -> Buffer.add_char buff c
       done;
       Buffer.contents buff
 
+  let sanitize_name s =
+    let rec loop esc i =
+      if i < 0 then if esc then escaped s else s
+      else match s.[i] with
+      | 'a'..'z' | 'A'..'Z' | '0'..'9' | '.' | '_' -> loop esc (i-1)
+      | '<' | '>' | '&' | '\'' | '\"' -> loop true (i-1)
+      | _ ->
+        (* This name contains complex characters:
+           this is probably a notation string, we simply hash it. *)
+        Digest.to_hex (Digest.string s)
+    in loop false (String.length s - 1)
+
   let latex_char _ = ()
   let latex_string _ = ()
 
@@ -618,19 +642,19 @@ module Html = struct
   let ident_ref m fid typ s =
     match find_module m with
     | Local ->
-	printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid;
-	printf "<span class=\"id\" type=\"%s\">%s</span></a>" typ s
+	printf "<a class=\"idref\" href=\"%s.html#%s\">" m (sanitize_name fid);
+	printf "<span class=\"id\" title=\"%s\">%s</span></a>" typ s
     | External m when !externals ->
-	printf "<a class=\"idref\" href=\"%s.html#%s\">" m fid;
-	printf "<span class=\"id\" type=\"%s\">%s</span></a>" typ s
+	printf "<a class=\"idref\" href=\"%s.html#%s\">" m (sanitize_name fid);
+	printf "<span class=\"id\" title=\"%s\">%s</span></a>" typ s
     | External _ | Unknown ->
-	printf "<span class=\"id\" type=\"%s\">%s</span>" typ s
+	printf "<span class=\"id\" title=\"%s\">%s</span>" typ s
 
   let reference s r =
     match r with
     | Def (fullid,ty) ->
-	printf "<a name=\"%s\">" fullid;
-	printf "<span class=\"id\" type=\"%s\">%s</span></a>" (type_name ty) s
+	printf "<a name=\"%s\">" (sanitize_name fullid);
+	printf "<span class=\"id\" title=\"%s\">%s</span></a>" (type_name ty) s
     | Ref (m,fullid,ty) ->
 	ident_ref m fullid (type_name ty) s
 
@@ -640,7 +664,7 @@ module Html = struct
     | Some ref -> reference s ref
     | None ->
 	if issymbchar then output_string s
-	else printf "<span class=\"id\" type=\"var\">%s</span>" s
+	else printf "<span class=\"id\" title=\"var\">%s</span>" s
 
   let sublexer c loc =
     let tag =
@@ -648,6 +672,9 @@ module Html = struct
     in
     Tokens.output_tagged_symbol_char tag c
 
+  let sublexer_in_doc c =
+    Tokens.output_tagged_symbol_char None c
+
   let initialize () =
     initialize_tex_html();
     Tokens.token_tree := token_tree_html;
@@ -657,16 +684,20 @@ module Html = struct
     match Tokens.translate s with Some s -> s | None -> escaped s
 
   let keyword s loc = 
-    printf "<span class=\"id\" type=\"keyword\">%s</span>" (translate s)
+    printf "<span class=\"id\" title=\"keyword\">%s</span>" (translate s)
 
   let ident s loc =
     if is_keyword s then begin
-      printf "<span class=\"id\" type=\"keyword\">%s</span>" (translate s)
+      printf "<span class=\"id\" title=\"keyword\">%s</span>" (translate s)
     end else begin
-      try reference (translate s) (Index.find (get_module false) loc)
+      try
+        match loc with
+        | None -> raise Not_found
+        | Some loc ->
+            reference (translate s) (Index.find (get_module false) loc)
       with Not_found ->
 	if is_tactic s then
-	  printf "<span class=\"id\" type=\"tactic\">%s</span>" (translate s)
+	  printf "<span class=\"id\" title=\"tactic\">%s</span>" (translate s)
 	else
 	  if !Cdglobals.interpolate && !in_doc (* always a var otherwise *)
 	  then
@@ -818,7 +849,7 @@ module Html = struct
 	       "[library]", m ^ ".html", t
 	else
 	 sprintf "[%s, in <a href=\"%s.html\">%s</a>]" (type_name t) m m ,
-	sprintf "%s.html#%s" m s, t)
+	sprintf "%s.html#%s" m (sanitize_name s), t)
 
   let format_bytype_index = function
     | Library, idx ->
@@ -827,7 +858,7 @@ module Html = struct
 	Index.map
 	  (fun s m ->
 	     let text = sprintf "[in <a href=\"%s.html\">%s</a>]" m m in
-	       (text, sprintf "%s.html#%s" m s, t)) idx
+	       (text, sprintf "%s.html#%s" m (sanitize_name s), t)) idx
 
   (* Impression de la table d'index *)
   let print_index_table_item i =
@@ -923,8 +954,6 @@ module TeXmacs = struct
   let (preamble : string Queue.t) =
     in_doc := false; Queue.create ()
 
-  let push_in_preamble s = Queue.add s preamble
-
   let header () =
     output_string
       "(*i This file has been automatically generated with the command  \n";
@@ -989,6 +1018,9 @@ module TeXmacs = struct
   let sublexer c l =
     if !in_doc then Tokens.output_tagged_symbol_char None c else char c
 
+  let sublexer_in_doc c =
+    char c
+
   let initialize () =
     Tokens.token_tree := token_tree_texmacs;
     Tokens.outfun := output_sublexer_string
@@ -1045,8 +1077,6 @@ module TeXmacs = struct
 
   let paragraph () = printf "\n\n"
 
-  let line_break_true () = printf "<format|line break>"
-
   let line_break () = printf "\n"
 
   let empty_line_of_code () = printf "\n"
@@ -1107,12 +1137,13 @@ module Raw = struct
   let stop_quote () = printf "\""
 
   let indentation n =
-      for i = 1 to n do printf " " done
+      for _i = 1 to n do printf " " done
 
   let keyword s loc = raw_ident s
   let ident s loc = raw_ident s
 
   let sublexer c l = char c
+  let sublexer_in_doc c = char c
 
   let initialize () =
     Tokens.token_tree := ref Tokens.empty_ttree;
@@ -1226,6 +1257,7 @@ let char = select Latex.char Html.char TeXmacs.char Raw.char
 let keyword = select Latex.keyword Html.keyword TeXmacs.keyword Raw.keyword
 let ident = select Latex.ident Html.ident TeXmacs.ident Raw.ident
 let sublexer = select Latex.sublexer Html.sublexer TeXmacs.sublexer Raw.sublexer
+let sublexer_in_doc = select Latex.sublexer_in_doc Html.sublexer_in_doc TeXmacs.sublexer_in_doc Raw.sublexer_in_doc
 let initialize = select Latex.initialize Html.initialize TeXmacs.initialize Raw.initialize
 
 let proofbox = select Latex.proofbox Html.proofbox TeXmacs.proofbox Raw.proofbox
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli
index 40fe69f7..c4628dd8 100644
--- a/tools/coqdoc/output.mli
+++ b/tools/coqdoc/output.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -61,8 +61,9 @@ val rule : unit -> unit
 val nbsp : unit -> unit
 val char : char -> unit
 val keyword : string -> loc -> unit
-val ident : string -> loc -> unit
+val ident : string -> loc option -> unit
 val sublexer : char -> loc -> unit
+val sublexer_in_doc : char -> unit
 val initialize : unit -> unit
 
 val proofbox : unit -> unit
diff --git a/tools/coqdoc/tokens.ml b/tools/coqdoc/tokens.ml
index 33560fce..a93ae855 100644
--- a/tools/coqdoc/tokens.ml
+++ b/tools/coqdoc/tokens.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -9,15 +9,16 @@
 (* Application of printing rules based on a dictionary specific to the
    target language *)
 
-open Cdglobals
-
 (*s Dictionaries: trees annotated with string options, each node being a map
     from chars to dictionaries (the subtrees). A trie, in other words.
 
     (code copied from parsing/lexer.ml4 for the use of coqdoc, Apr 2010)
 *)
 
-module CharMap = Map.Make (struct type t = char let compare = compare end)
+module CharMap = Map.Make (struct
+  type t = char
+  let compare (x : t) (y : t) = compare x y
+end)
 
 type ttree = {
   node : string option;
diff --git a/tools/coqdoc/tokens.mli b/tools/coqdoc/tokens.mli
index 898f2b5c..c4fe3bc8 100644
--- a/tools/coqdoc/tokens.mli
+++ b/tools/coqdoc/tokens.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)