diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-07-05 12:56:27 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-07-05 12:56:27 +0200 |
| commit | d19605b7bfb8425b53be4cab30bef462c4fa4d14 (patch) | |
| tree | 2bdcc15e217c24ca33b2fe48537c8632562a9ec1 /tools | |
| parent | 7413f8532879c64e05ee0e8ca16693d74fe84ab9 (diff) | |
| parent | 08b2fde7054a61e5468ef90eabb0d348730f170e (diff) | |
Merge PR #7746: Many small cleanups removing unused arguments and functions
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coq_makefile.ml | 4 | ||||
| -rw-r--r-- | tools/coqdoc/index.ml | 2 | ||||
| -rw-r--r-- | tools/coqdoc/index.mli | 2 | ||||
| -rw-r--r-- | tools/coqdoc/output.ml | 4 |
4 files changed, 6 insertions, 6 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 6f11ee397..ad489da82 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -218,7 +218,7 @@ let windrive s = else "" ;; -let generate_conf_coq_config oc args = +let generate_conf_coq_config oc = section oc "Coq configuration."; let src_dirs = Coq_config.all_src_dirs in Envars.print_config ~prefix_var_name:"COQMF_" oc src_dirs; @@ -282,7 +282,7 @@ let generate_conf oc project args = fprintf oc "# %s\n\n" (String.concat " " (List.map quote args)); generate_conf_files oc project; generate_conf_includes oc project; - generate_conf_coq_config oc args; + generate_conf_coq_config oc; generate_conf_defs oc project; generate_conf_doc oc project; generate_conf_extra_target oc project.extra_targets; diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml index df493fdf7..885324aa0 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 *) diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli index 5cd301389..7c9aad67f 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 d25227002..c640167ac 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -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 |