From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 tools/coqdoc/alpha.ml      | 29 +++++++++++-----------
 tools/coqdoc/alpha.mli     | 10 +++++---
 tools/coqdoc/cdglobals.ml  | 34 ++++++++++++-------------
 tools/coqdoc/cdglobals.mli | 49 ++++++++++++++++++++++++++++++++++++
 tools/coqdoc/cpretty.mli   | 10 +++++---
 tools/coqdoc/cpretty.mll   | 29 ++++++++++++++--------
 tools/coqdoc/index.ml      | 30 +++++++++++++---------
 tools/coqdoc/index.mli     | 10 +++++---
 tools/coqdoc/main.ml       | 10 +++++---
 tools/coqdoc/output.ml     | 62 ++++++++++++++++++++++++----------------------
 tools/coqdoc/output.mli    | 11 ++++----
 tools/coqdoc/tokens.ml     | 10 +++++---
 tools/coqdoc/tokens.mli    | 10 +++++---
 13 files changed, 192 insertions(+), 112 deletions(-)
 create mode 100644 tools/coqdoc/cdglobals.mli

(limited to 'tools/coqdoc')

diff --git a/tools/coqdoc/alpha.ml b/tools/coqdoc/alpha.ml
index f817ed5a..269c1a1d 100644
--- a/tools/coqdoc/alpha.ml
+++ b/tools/coqdoc/alpha.ml
@@ -1,14 +1,20 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Cdglobals
 
-let norm_char_latin1 c = match Char.uppercase c with
+[@@@ocaml.warning "-3"]       (* Char.uppercase_ascii since 4.03.0 GPR#124 *)
+let uppercase = Char.uppercase
+[@@@ocaml.warning "+3"]
+
+let norm_char_latin1 c = match uppercase c with
   | '\192'..'\198' -> 'A'
   | '\199' -> 'C'
   | '\200'..'\203' -> 'E'
@@ -19,19 +25,14 @@ let norm_char_latin1 c = match Char.uppercase c with
   | '\221' -> 'Y'
   | c -> c
 
-let norm_char_utf8 c = Char.uppercase c
+let norm_char_utf8 c = uppercase c
 
 let norm_char c =
   if !utf8 then norm_char_utf8 c else
   if !latin1 then norm_char_latin1 c else
-  Char.uppercase c
-
-let norm_string s =
-  let u = String.copy s in
-  for i = 0 to String.length s - 1 do
-    u.[i] <- norm_char s.[i]
-  done;
-  u
+  uppercase c
+
+let norm_string = String.map (fun s -> norm_char s)
 
 let compare_char c1 c2 = match norm_char c1, norm_char c2 with
   | ('A'..'Z' as c1), ('A'..'Z' as c2) -> compare c1 c2
diff --git a/tools/coqdoc/alpha.mli b/tools/coqdoc/alpha.mli
index f6d47a55..86303450 100644
--- a/tools/coqdoc/alpha.mli
+++ b/tools/coqdoc/alpha.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (* Alphabetic order. *)
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index 5d48473d..0d3fb775 100644
--- a/tools/coqdoc/cdglobals.ml
+++ b/tools/coqdoc/cdglobals.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 
@@ -70,23 +72,21 @@ let normalize_filename f =
   let dirname = Filename.dirname f in
   normalize_path dirname, basename
 
+(** Add a local installation suffix (unless the suffix is itself
+    absolute in which case the prefix does not matter) *)
+let use_suffix prefix suffix =
+  if String.length suffix > 0 && suffix.[0] = '/' then suffix else prefix / suffix
+
 (** A weaker analog of the function in Envars *)
 
 let guess_coqlib () =
   let file = "theories/Init/Prelude.vo" in
-  match Coq_config.coqlib with
-    | 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_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 coqbin = normalize_path (Filename.dirname Sys.executable_name) in
+  let prefix = Filename.dirname coqbin in
+  let coqlib = use_suffix prefix Coq_config.coqlibsuffix in
+  if Sys.file_exists (coqlib / file) then coqlib else
+  if not Coq_config.local && Sys.file_exists (Coq_config.coqlib / file)
+  then Coq_config.coqlib else prefix
 
 let header_trailer = ref true
 let header_file = ref ""
diff --git a/tools/coqdoc/cdglobals.mli b/tools/coqdoc/cdglobals.mli
new file mode 100644
index 00000000..2c9b3fb8
--- /dev/null
+++ b/tools/coqdoc/cdglobals.mli
@@ -0,0 +1,49 @@
+type target_language = LaTeX | HTML | TeXmacs | Raw
+val target_language : target_language ref
+type output_t = StdOut | MultFiles | File of string
+val output_dir : string ref
+val out_to : output_t ref
+val out_channel : out_channel ref
+val ( / ) : string -> string -> string
+val coqdoc_out : string -> string
+val open_out_file : string -> unit
+val close_out_file : unit -> unit
+type glob_source_t = NoGlob | DotGlob | GlobFile of string
+val glob_source : glob_source_t ref
+val normalize_path : string -> string
+val normalize_filename : string -> string * string
+val guess_coqlib : unit -> string
+val header_trailer : bool ref
+val header_file : string ref
+val header_file_spec : bool ref
+val footer_file : string ref
+val footer_file_spec : bool ref
+val quiet : bool ref
+val light : bool ref
+val gallina : bool ref
+val short : bool ref
+val index : bool ref
+val multi_index : bool ref
+val index_name : string ref
+val toc : bool ref
+val page_title : string ref
+val title : string ref
+val externals : bool ref
+val coqlib : string ref
+val coqlib_path : string ref
+val raw_comments : bool ref
+val parse_comments : bool ref
+val plain_comments : bool ref
+val toc_depth : int option ref
+val lib_name : string ref
+val lib_subtitles : bool ref
+val interpolate : bool ref
+val inline_notmono : bool ref
+val charset : string ref
+val inputenc : string ref
+val latin1 : bool ref
+val utf8 : bool ref
+val set_latin1 : unit -> unit
+val set_utf8 : unit -> unit
+type coq_module = string
+type file = Vernac_file of string * coq_module | Latex_file of string
diff --git a/tools/coqdoc/cpretty.mli b/tools/coqdoc/cpretty.mli
index 58b19184..7732610f 100644
--- a/tools/coqdoc/cpretty.mli
+++ b/tools/coqdoc/cpretty.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 val coq_file : string -> Cdglobals.coq_module -> unit
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 919f37b9..1be440a7 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (*s Utility functions for the scanners *)
@@ -682,7 +684,7 @@ and doc_bol = parse
   | space* nl+
       { Output.paragraph (); doc_bol lexbuf }
   | "<<" space*
-      { Output.start_verbatim false; verbatim false lexbuf; doc_bol lexbuf }
+      { Output.start_verbatim false; verbatim 0 false lexbuf; doc_bol lexbuf }
   | eof
       { true }
   | '_'
@@ -707,7 +709,7 @@ and doc_list_bol indents = parse
       }
   | "<<" space*
       { Output.start_verbatim false;
-        verbatim false lexbuf;
+        verbatim 0 false lexbuf;
         doc_list_bol indents lexbuf }
   | "[[" nl
       { formatted := true;
@@ -852,7 +854,7 @@ and doc indents = parse
         Output.char (lexeme_char lexbuf 1);
         doc indents lexbuf }
   | "<<" space*
-      { Output.start_verbatim true; verbatim true lexbuf; doc_bol lexbuf }
+      { Output.start_verbatim true; verbatim 0 true lexbuf; doc_bol lexbuf }
   | '"'
       { if !Cdglobals.plain_comments 
 	then Output.char '"' 
@@ -892,13 +894,20 @@ and escaped_html = parse
         { backtrack lexbuf }
   | _   { Output.html_char (lexeme_char lexbuf 0); escaped_html lexbuf }
 
-and verbatim inline = parse
+and verbatim depth 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 }
+  | "(*" { Output.verbatim_char inline '(';
+           Output.verbatim_char inline '*';
+           verbatim (depth+1) inline lexbuf }
+  | "*)" { if (depth == 0)
+           then (Output.stop_verbatim inline; backtrack lexbuf)
+           else (Output.verbatim_char inline '*';
+                 Output.verbatim_char inline ')';
+                 verbatim (depth-1) inline lexbuf) }
   | eof { Output.stop_verbatim inline }
-  | _ { Output.verbatim_char inline (lexeme_char lexbuf 0); verbatim inline lexbuf }
+  | _ { Output.verbatim_char inline (lexeme_char lexbuf 0); verbatim depth inline lexbuf }
 
 and url = parse
   | "}}" { Output.url (Buffer.contents url_buffer) None; Buffer.clear url_buffer }
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index 9be791a8..df493fdf 100644
--- a/tools/coqdoc/index.ml
+++ b/tools/coqdoc/index.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Printf
@@ -117,7 +119,7 @@ let find_module m =
   if Hashtbl.mem local_modules m then
     Local
   else
-    try External (Filename.concat (find_external_library m) m)
+    try External (find_external_library m ^ "/" ^ m)
     with Not_found -> Unknown
 
 
@@ -155,10 +157,14 @@ let sort_entries el =
 
 let display_letter c = if c = '*' then "other" else String.make 1 c
 
+[@@@ocaml.warning "-3"]       (* String.lowercase_ascii since 4.03.0 GPR#124 *)
+let lowercase = String.lowercase
+[@@@ocaml.warning "+3"]
+
 let type_name = function
   | Library ->
       let ln = !lib_name in
-        if ln <> "" then String.lowercase ln else "library"
+        if ln <> "" then lowercase ln else "library"
   | Module -> "module"
   | Definition -> "definition"
   | Inductive -> "inductive"
@@ -197,7 +203,7 @@ let prepare_entry s = function
       let h = try String.index_from s 0 ':' with _ -> err () in
       let i = try String.index_from s (h+1) ':' with _ -> err () in
       let sc = String.sub s (h+1) (i-h-1) in
-      let ntn = String.make (String.length s - i) ' ' in
+      let ntn = Bytes.make (String.length s - i) ' ' in
       let k = ref 0 in
       let j = ref (i+1) in
       let quoted = ref false in
@@ -205,22 +211,22 @@ let prepare_entry s = function
       while !j <= l do
 	if not !quoted then begin
 	  (match s.[!j] with
-	  | '_' -> ntn.[!k] <- ' '; incr k
-	  | 'x' -> ntn.[!k] <- '_'; incr k
+	  | '_' -> Bytes.set ntn !k ' '; incr k
+	  | 'x' -> Bytes.set ntn !k '_'; incr k
 	  | '\'' -> quoted := true
 	  | _ -> assert false)
 	end
 	else
 	  if s.[!j] = '\'' then
 	    if (!j = l || s.[!j+1] = '_') then quoted := false
-	    else (incr j; ntn.[!k] <- s.[!j]; incr k)
+	    else (incr j; Bytes.set ntn !k s.[!j]; incr k)
 	  else begin
-	    ntn.[!k] <- s.[!j];
+	    Bytes.set ntn !k s.[!j];
 	    incr k
 	  end;
 	incr j
       done;
-      let ntn = String.sub ntn 0 !k in
+      let ntn = Bytes.sub_string ntn 0 !k in
       if sc = "" then ntn else ntn ^ " (" ^ sc ^ ")"
   | _ ->
       s
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli
index e44bbd59..5cd30138 100644
--- a/tools/coqdoc/index.mli
+++ b/tools/coqdoc/index.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Cdglobals
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index fe438738..11ec3d39 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (* Modified by Lionel Elie Mamane <lionel@mamane.lu> on 9 & 10 Mar 2004:
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 82d3d62b..d2522700 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Cdglobals
@@ -19,6 +21,10 @@ let printf s = Printf.fprintf !out_channel s
 
 let sprintf = Printf.sprintf
 
+[@@@ocaml.warning "-3"]       (* String.{capitalize,lowercase}_ascii since 4.03.0 GPR#124 *)
+let capitalize = String.capitalize
+let lowercase = String.lowercase
+[@@@ocaml.warning "+3"]
 
 (*s Coq keywords *)
 
@@ -36,7 +42,7 @@ let is_keyword =
       "Hypothesis"; "Hypotheses";
       "Resolve"; "Unfold"; "Immediate"; "Extern"; "Constructors"; "Rewrite";
       "Implicit"; "Import"; "Inductive";
-      "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Ltac";
+      "Infix"; "Lemma"; "Let"; "Load"; "Local"; "Locate"; "Ltac";
       "Module"; "Module Type"; "Declare Module"; "Include";
       "Mutual"; "Parameter"; "Parameters"; "Print"; "Printing"; "All"; "Proof"; "Proof with"; "Qed";
       "Record"; "Recursive"; "Remark"; "Require"; "Save"; "Scheme"; "Assumptions"; "Axioms"; "Universes";
@@ -58,9 +64,9 @@ let is_keyword =
       (*i (* coq terms *) *)
       "forall"; "match"; "as"; "in"; "return"; "with"; "end"; "let"; "fun";
       "if"; "then"; "else"; "Prop"; "Set"; "Type"; ":="; "where"; "struct"; "wf"; "measure";
-      "fix"; "cofix";
+      "fix"; "cofix"; "is";
       (* Ltac *)
-      "before"; "after"; "constr"; "ltac"; "goal"; "context"; "beta"; "delta"; "iota"; "zeta"; "lazymatch";
+      "before"; "after"; "constr"; "ltac"; "goal"; "context"; "beta"; "delta"; "iota"; "zeta"; "lazymatch"; "type"; "of"; "rec";
       (* Notations *)
       "level"; "associativity"; "no"
        ]
@@ -70,7 +76,7 @@ let is_tactic =
     [ "intro"; "intros"; "apply"; "rewrite"; "refine"; "case"; "clear"; "injection";
       "elimtype"; "progress"; "setoid_rewrite"; "left"; "right"; "constructor"; 
       "econstructor"; "decide equality"; "abstract"; "exists"; "cbv"; "simple destruct";
-      "info"; "fourier"; "field"; "specialize"; "evar"; "solve"; "instanciate";
+      "info"; "fourier"; "field"; "specialize"; "evar"; "solve"; "instanciate"; "info_auto"; "info_eauto";
       "quote"; "eexact"; "autorewrite";
       "destruct"; "destruction"; "destruct_call"; "dependent"; "elim"; "extensionality";
       "f_equal"; "generalize"; "generalize_eqs"; "generalize_eqs_vars"; "induction"; "rename"; "move"; "omega";
@@ -689,25 +695,21 @@ module Html = struct
     printf "<span class=\"id\" title=\"keyword\">%s</span>" (translate s)
 
   let ident s loc =
-    if is_keyword s then begin
-      printf "<span class=\"id\" title=\"keyword\">%s</span>" (translate s)
-    end else begin
-      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\" title=\"tactic\">%s</span>" (translate s)
-	else
-	  if !Cdglobals.interpolate && !in_doc (* always a var otherwise *)
-	  then
-	    try reference (translate s) (Index.find_string (get_module false) s)
-	    with _ -> Tokens.output_tagged_ident_string s
-	  else
-	    Tokens.output_tagged_ident_string s
-    end
+    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\" title=\"tactic\">%s</span>" (translate s)
+      else if is_keyword s then
+        printf "<span class=\"id\" title=\"keyword\">%s</span>" (translate s)
+      else if !Cdglobals.interpolate && !in_doc (* always a var otherwise *) then
+	try reference (translate s) (Index.find_string (get_module false) s)
+	with Not_found -> Tokens.output_tagged_ident_string s
+      else
+	Tokens.output_tagged_ident_string s
 
   let proofbox () = printf "<font size=-2>&#9744;</font>"
 
@@ -846,7 +848,7 @@ module Html = struct
 	if t = Library then
          let ln = !lib_name in
            if ln <> "" then
-	       "[" ^ String.lowercase ln ^ "]", m ^ ".html", t
+	       "[" ^ lowercase ln ^ "]", m ^ ".html", t
            else
 	       "[library]", m ^ ".html", t
 	else
@@ -864,7 +866,7 @@ module Html = struct
 
   (* Impression de la table d'index *)
   let print_index_table_item i =
-    printf "<tr>\n<td>%s Index</td>\n" (String.capitalize i.idx_name);
+    printf "<tr>\n<td>%s Index</td>\n" (capitalize i.idx_name);
     List.iter
       (fun (c,l) ->
 	 if l <> [] then
@@ -912,7 +914,7 @@ module Html = struct
     let print_table () = print_index_table all_index in
     let print_one_index i =
       if i.idx_size > 0 then begin
-	printf "<hr/>\n<h1>%s Index</h1>\n" (String.capitalize i.idx_name);
+	printf "<hr/>\n<h1>%s Index</h1>\n" (capitalize i.idx_name);
 	all_letters i
       end
     in
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli
index 853bc29a..a8a50d75 100644
--- a/tools/coqdoc/output.mli
+++ b/tools/coqdoc/output.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Cdglobals
@@ -64,7 +66,6 @@ val keyword : 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 b6a1057a..49f7ef2f 100644
--- a/tools/coqdoc/tokens.ml
+++ b/tools/coqdoc/tokens.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (* Application of printing rules based on a dictionary specific to the
diff --git a/tools/coqdoc/tokens.mli b/tools/coqdoc/tokens.mli
index f07efedf..00db2ad3 100644
--- a/tools/coqdoc/tokens.mli
+++ b/tools/coqdoc/tokens.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (* Type of dictionaries *)
-- 
cgit v1.2.3