diff options
| author | coqbot-app[bot] | 2020-12-30 17:44:42 +0000 |
|---|---|---|
| committer | GitHub | 2020-12-30 17:44:42 +0000 |
| commit | d338a65ce7c4619ecc238c091a409175f5330d8f (patch) | |
| tree | 590a7d3e0a5c8e1df4f017a1956214354680b690 | |
| parent | 30f648dc29958add42e7509a9c29f271f768e183 (diff) | |
| parent | aed648afd2cf8b09d67fb39c9672b71166089395 (diff) | |
Merge PR #13682: Fix broken HTML rendering of inference rules (fix #12783).
Reviewed-by: herbelin
| -rw-r--r-- | test-suite/coqdoc/verbatim.html.out | 2 | ||||
| -rw-r--r-- | tools/coqdoc/output.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/coqdoc/verbatim.html.out b/test-suite/coqdoc/verbatim.html.out index bf9f975ee8..070f80e771 100644 --- a/test-suite/coqdoc/verbatim.html.out +++ b/test-suite/coqdoc/verbatim.html.out @@ -90,7 +90,7 @@ verbatim <tr class="infruleassumption"> <td class="infrule">Γ ⊢ A ∨ B</td> <td></td> -</td> +</tr> </table></center> <div class="paragraph"> </div> diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index a87dfb5b2e..10edb0b4db 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -783,7 +783,7 @@ module Html = struct printf " <td class=\"infrule\">%s</td>\n" (replace_spaces line)) in let end_assumption () = (printf " <td></td>\n"; - printf "</td>\n") in + printf "</tr>\n") in let rec print_assumptions hyps = match hyps with | [] -> start_assumption " " |