Fix printing of the QED step.

Signed-off-by: Karolis Petrauskas <[email protected]>
tlaplus · Oct 2, 2024 · b8b2611 · b8b2611
1 parent caefe81
commit b8b2611
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/proof/p_fmt.ml b/src/proof/p_fmt.ml
@@ -125,7 +125,7 @@ let rec pp_print_proof cx ff prf =
                    cx)
                 cx ff inits
             in
-            fprintf ff "@[<hv2>%s%s QED%a@]"
+            fprintf ff "@[<hv2>%s%s QED %a@]"
               (step_name prf) (step_dot prf)
               (pp_print_qed_step(*proof_nl*) cx) qed
         | Error msg ->