From b6089e67c32bb2b3d847f4a827e123836c873733 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Thu, 29 Jan 2015 15:14:24 +0100
Subject: [PATCH] Fix for bad html printing

---
 solver/mcproof.ml | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

diff --git a/solver/mcproof.ml b/solver/mcproof.ml
index 6e174359..7f6aabc9 100644
--- a/solver/mcproof.ml
+++ b/solver/mcproof.ml
@@ -350,10 +350,15 @@ module Make(St : Mcsolver_types.S) = struct
         let name, f_args, t_args, color = St.proof_debug proof in
         let color = match color with None -> "YELLOW" | Some c -> c in
         let aux fmt () =
-          Format.fprintf fmt "<TR><TD colspan=\"2\">%a</TD></TR><TR><TD BGCOLOR=\"%s\" rowspan=\"%d\">%s</TD>%a%a</TR>"
-            print_clause p.conclusion color (List.length f_args + List.length t_args) name
-            (fun fmt -> List.iter (fun a -> Format.fprintf fmt "<TD>%a</TD>" St.print_atom a)) f_args
-            (fun fmt -> List.iter (fun v -> Format.fprintf fmt "<TD>%a</TD>" St.print_semantic_var v)) t_args
+          Format.fprintf fmt "<TR><TD colspan=\"2\">%a</TD></TR><TR><TD BGCOLOR=\"%s\" rowspan=\"%d\">%s</TD>"
+            print_clause p.conclusion color (List.length f_args + List.length t_args) name;
+          if f_args <> [] then
+              Format.fprintf fmt "<TD>%a</TD>%a%a" St.print_atom (List.hd f_args)
+                (fun fmt -> List.iter (fun a -> Format.fprintf fmt "<TR><TD>%a</TD></TR>" St.print_atom a)) (List.tl f_args)
+                (fun fmt -> List.iter (fun v -> Format.fprintf fmt "<TR><TD>%a</TD></TR>" St.print_semantic_var v)) t_args
+          else
+              Format.fprintf fmt "<TD>%a</TD>%a" St.print_semantic_var (List.hd t_args)
+                (fun fmt -> List.iter (fun v -> Format.fprintf fmt "<TR><TD>%a</TD></TR>" St.print_semantic_var v)) (List.tl t_args)
         in
         print_dot_rule "BGCOLOR=\"LIGHTBLUE\"" aux () fmt p.conclusion
       | Resolution (proof1, proof2, a) ->