diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-04-06 16:01:44 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-04-06 16:01:44 +0200 |
| commit | 4f8ba5f0651eb986a63ffc58c072ed06fac0f53b (patch) | |
| tree | 76b8380685e31b59ab6134fd14e42cce4a15daa9 /doc | |
| parent | 41b17255f3517b875c19cb7b5c340b88f77da920 (diff) | |
| download | compcert-kvx-4f8ba5f0651eb986a63ffc58c072ed06fac0f53b.tar.gz compcert-kvx-4f8ba5f0651eb986a63ffc58c072ed06fac0f53b.zip | |
Also enable warnings for doc generator.
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/coq2html.mll | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/doc/coq2html.mll b/doc/coq2html.mll index 7dd93842..a5b284e2 100644 --- a/doc/coq2html.mll +++ b/doc/coq2html.mll @@ -60,9 +60,9 @@ let shortname m = Str.replace_first re_shortname "" m let crossref m pos = (*eprintf "crossref %s %d\n" m pos;*) try match Hashtbl.find xref_table (m, pos) with - | Def(p, ty) -> + | Def(p, _) -> Anchor p - | Ref(m', p, ty) -> + | Ref(m', p, _) -> let url = if Hashtbl.mem xref_modules m' then shortname m' ^ ".html" @@ -152,7 +152,7 @@ let end_doc_right () = let enum_depth = ref 0 -let rec set_enum_depth d = +let set_enum_depth d = if !enum_depth < d then begin fprintf !oc "<ul>\n"; fprintf !oc "<li>\n"; @@ -188,7 +188,7 @@ let ident pos id = fprintf !oc "<span class=\"id\"><a name=\"%s\">%s</a></span>" p id let space s = - for i = 1 to String.length s do fprintf !oc " " done + for _ = 1 to String.length s do fprintf !oc " " done let newline () = fprintf !oc "<br/>\n" @@ -396,7 +396,7 @@ and globfile = parse | "F" (path as m) space* "\n" { current_module := m; add_module m; globfile lexbuf } - | "R" (integer as pos) ":" (integer as pos2) + | "R" (integer as pos) ":" (integer) space+ (xref as dp) space+ (xref as sp) space+ (xref as id) @@ -405,7 +405,7 @@ and globfile = parse { add_reference !current_module (int_of_string pos) dp sp id ty; globfile lexbuf } | (ident as ty) - space+ (integer as pos) ":" (integer as pos2) + space+ (integer as pos) ":" (integer) space+ (xref as sp) space+ (xref as id) space* "\n" |