From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- tools/coqdoc/alpha.ml | 2 +- tools/coqdoc/alpha.mli | 2 +- tools/coqdoc/cdglobals.ml | 22 +++++++----- tools/coqdoc/coqdoc.css | 63 +++++++++++++++++++++++++++++--- tools/coqdoc/coqdoc.sty | 2 +- tools/coqdoc/cpretty.mli | 4 +-- tools/coqdoc/cpretty.mll | 60 ++++++++++++------------------- tools/coqdoc/index.ml | 44 +++-------------------- tools/coqdoc/index.mli | 2 +- tools/coqdoc/main.ml | 9 +++-- tools/coqdoc/output.ml | 92 +++++++++++++++++++++++++++++++---------------- tools/coqdoc/output.mli | 5 +-- tools/coqdoc/tokens.ml | 9 ++--- tools/coqdoc/tokens.mli | 2 +- 14 files changed, 183 insertions(+), 135 deletions(-) (limited to 'tools/coqdoc') 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 *) -(* "" && 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: ) */ + .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 (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 *) -(* 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 *) -(* 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 *) -(* "" | 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 *) -(* set the path where Coq files are installed"; prerr_endline " -R map physical dir to Coq dir"; + prerr_endline " -Q 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 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 *) -(* () | 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 "\n"; printf "\n\n"; - printf "\n" !charset; - printf "\n"; + printf "\n" !charset; + printf "\n"; printf "%s\n\n\n" !page_title; printf "\n\n
\n\n
\n
\n\n"; printf "
\n\n" @@ -558,7 +571,7 @@ module Html = struct printf "

%s %s

\n\n" ln (get_module true) end - let indentation n = for i = 1 to n do printf " " done + let indentation n = for _i = 1 to n do printf " " done let line_break () = printf "
\n" @@ -573,9 +586,6 @@ module Html = struct | '&' -> printf "&" | 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 "<" | '>' -> Buffer.add_string buff ">" | '&' -> Buffer.add_string buff "&" + | '\'' -> Buffer.add_string buff "´" + | '\"' -> Buffer.add_string buff """ | 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 "" m fid; - printf "%s" typ s + printf "" m (sanitize_name fid); + printf "%s" typ s | External m when !externals -> - printf "" m fid; - printf "%s" typ s + printf "" m (sanitize_name fid); + printf "%s" typ s | External _ | Unknown -> - printf "%s" typ s + printf "%s" typ s let reference s r = match r with | Def (fullid,ty) -> - printf "" fullid; - printf "%s" (type_name ty) s + printf "" (sanitize_name fullid); + printf "%s" (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 "%s" s + else printf "%s" 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 "%s" (translate s) + printf "%s" (translate s) let ident s loc = if is_keyword s then begin - printf "%s" (translate s) + printf "%s" (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 "%s" (translate s) + printf "%s" (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 %s]" (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 %s]" 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 "" - 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 *) -(* 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 *) -(*