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 | |
| parent | 41b17255f3517b875c19cb7b5c340b88f77da920 (diff) | |
| download | compcert-4f8ba5f0651eb986a63ffc58c072ed06fac0f53b.tar.gz compcert-4f8ba5f0651eb986a63ffc58c072ed06fac0f53b.zip | |
Also enable warnings for doc generator.
| -rw-r--r-- | Makefile | 4 | ||||
| -rw-r--r-- | doc/coq2html.mll | 12 |
2 files changed, 8 insertions, 8 deletions
@@ -166,7 +166,7 @@ documentation: doc/coq2html $(FILES) cp doc/coq2html.css doc/coq2html.js doc/html/ doc/coq2html: doc/coq2html.ml - ocamlopt -o doc/coq2html str.cmxa doc/coq2html.ml + ocamlopt -w +a-29 -o doc/coq2html str.cmxa doc/coq2html.ml doc/coq2html.ml: doc/coq2html.mll ocamllex -q doc/coq2html.mll @@ -262,7 +262,7 @@ check-admitted: $(FILES) # UnionFind.UF.elt gives "Anomaly: Uncaught exception Reduction.NotConvertible" check-proof: $(FILES) - $(COQCHK) -admit Integers -admit Floats -admit AST -admit Asm -admit Mach -admit UnionFind Complements + $(COQCHK) -admit Integers -admit Floats -admit AST -admit Asm -admit Mach -admit UnionFind Complements print-includes: @echo $(COQINCLUDES) 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" |