aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
authorGuillaume Melquiond2020-12-28 10:29:34 +0100
committerGuillaume Melquiond2020-12-28 11:26:54 +0100
commitaed648afd2cf8b09d67fb39c9672b71166089395 (patch)
treeec0776c32d6ed1da21dc4a2f462b8f6ef09450df /tools
parent52154bfa574b30c10a9fbd78584cca44b885dc60 (diff)
Fix broken HTML rendering of inference rules (fix #12783).
Diffstat (limited to 'tools')
-rw-r--r--tools/coqdoc/output.ml2
1 files changed, 1 insertions, 1 deletions
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 "&nbsp;&nbsp;"