Fixed nasty bug in maxvar updating

[helm.git] / helm / software / components / ng_paramodulation / pp.ml

diff --git a/helm/software/components/ng_paramodulation/pp.ml b/helm/software/components/ng_paramodulation/pp.ml
index 2e95e7a95316c0c158e3e36bc9629f883d0a11e5..537ad02c13e849e6044a1d7a4512f55da4b33d2f 100644 (file)
--- a/helm/software/components/ng_paramodulation/pp.ml
+++ b/helm/software/components/ng_paramodulation/pp.ml
@@ -47,12 +47,14 @@ let string_of_direction = function
 ;;
 
 let pp_substitution ~formatter:f subst =
-     (List.iter
-       (fun (i, t) ->
-          (Format.fprintf f "?%d -> " i;
-          pp_foterm f t)
-       )
-       subst)
+  Format.fprintf f "@[<v 2>";
+  List.iter
+    (fun (i, t) ->
+       (Format.fprintf f "?%d -> " i;
+       pp_foterm f t;
+       Format.fprintf f "@;"))
+    subst;
+  Format.fprintf f "@]";
 ;;
 
 let pp_proof bag ~formatter:f p =