Imported Upstream version 8.9.0upstream/8.9.0upstream

3 files changed, 14 insertions, 10 deletions

diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index df493fdf..724d3838 100644
--- a/tools/coqdoc/index.ml
+++ b/tools/coqdoc/index.ml
@@ -77,7 +77,7 @@ let add_ref m loc m' sp id ty =
 
 let find m l = Hashtbl.find reftable (m, l)
 
-let find_string m s = let (m,s,t) = Hashtbl.find byidtable s in Ref (m,s,t)
+let find_string s = let (m,s,t) = Hashtbl.find byidtable s in Ref (m,s,t)
 
 (* Coq modules *)
 
@@ -185,7 +185,8 @@ let type_name = function
 let prepare_entry s = function
   | Notation ->
       (* We decode the encoding done in Dumpglob.cook_notation of coqtop *)
-      (* Encoded notations have the form section:sc:x_'++'_x where:      *)
+      (* Encoded notations have the form section:entry:sc:x_'++'_x       *)
+      (* where:                                                          *)
       (* - the section, if any, ends with a "."                          *)
       (* - the scope can be empty                                        *)
       (* - tokens are separated with "_"                                 *)
@@ -202,10 +203,12 @@ let prepare_entry s = function
       let err () = eprintf "Invalid notation in globalization file\n"; exit 1 in
       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 = Bytes.make (String.length s - i) ' ' in
+      let m = try String.index_from s (i+1) ':' with _ -> err () in
+      let entry = String.sub s (h+1) (i-h-1) in
+      let sc = String.sub s (i+1) (m-i-1) in
+      let ntn = Bytes.make (String.length s - m) ' ' in
       let k = ref 0 in
-      let j = ref (i+1) in
+      let j = ref (m+1) in
       let quoted = ref false in
       let l = String.length s - 1 in
       while !j <= l do
@@ -227,7 +230,8 @@ let prepare_entry s = function
 	incr j
       done;
       let ntn = Bytes.sub_string ntn 0 !k in
-      if sc = "" then ntn else ntn ^ " (" ^ sc ^ ")"
+      let ntn = if sc = "" then ntn else ntn ^ " (" ^ sc ^ ")" in
+      if entry = "" then ntn else entry ^ ":" ^ ntn
   | _ ->
       s
 
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli
index 5cd30138..7c9aad67 100644
--- a/tools/coqdoc/index.mli
+++ b/tools/coqdoc/index.mli
@@ -41,7 +41,7 @@ type index_entry =
 val find : coq_module -> loc -> index_entry
 
 (* Find what data is referred to by some string in some coq module *)
-val find_string : coq_module -> string -> index_entry
+val find_string : string -> index_entry
 
 val add_module : coq_module -> unit
 
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index d2522700..750698a1 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -76,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_auto"; "info_eauto";
+      "info"; "field"; "specialize"; "evar"; "solve"; "instantiate"; "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";
@@ -431,7 +431,7 @@ module Latex = struct
       else if !Cdglobals.interpolate && !in_doc (* always a var otherwise *)
       then
 	try
-	  let tag = Index.find_string (get_module false) s in
+          let tag = Index.find_string s in
 	  reference (translate s) tag
 	with _ -> Tokens.output_tagged_ident_string s
       else Tokens.output_tagged_ident_string s
@@ -706,7 +706,7 @@ module Html = struct
       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)
+        try reference (translate s) (Index.find_string s)
 	with Not_found -> Tokens.output_tagged_ident_string s
       else
 	Tokens.output_tagged_ident_string s