From aed648afd2cf8b09d67fb39c9672b71166089395 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Mon, 28 Dec 2020 10:29:34 +0100
Subject: Fix broken HTML rendering of inference rules (fix #12783).

---
 test-suite/coqdoc/verbatim.html.out | 2 +-
 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 "&nbsp;&nbsp;"
-- 
cgit v1.2.3