Make figures fit onto the page

1 files changed, 19 insertions, 10 deletions

diff --git a/proof.tex b/proof.tex
index 850e225..58a5417 100644
--- a/proof.tex
+++ b/proof.tex
@@ -27,8 +27,10 @@ As HTL is quite different to RTL, this first translation is the most involved tr
 \begin{figure}
   \centering
 \begin{minted}{coq}
-Inductive match_states : RTL.state -> HTL.state -> Prop :=
-| match_state : forall asa asr sf f sp sp' rs mem m st res
+Inductive match_states :
+  RTL.state -> HTL.state -> Prop :=
+| match_state : forall asa asr sf f sp
+    sp' rs mem m st res
     (MASSOC : match_assocmaps f rs asr)
     (TF : tr_module f m)
     (WF : state_st_wf m (HTL.State res m st asr asa))
@@ -36,17 +38,24 @@ Inductive match_states : RTL.state -> HTL.state -> Prop :=
     (MARR : match_arrs m f sp mem asa)
     (SP : sp = Values.Vptr sp' (Integers.Ptrofs.repr 0))
     (RSBP : reg_stack_based_pointers sp' rs)
-    (ASBP : arr_stack_based_pointers sp' mem (f.(RTL.fn_stacksize)) sp)
+    (ASBP : arr_stack_based_pointers sp' mem
+              (f.(RTL.fn_stacksize)) sp)
     (BOUNDS : stack_bounds sp (f.(RTL.fn_stacksize)) mem)
     (CONST : match_constants m asr),
-    match_states (RTL.State sf f sp st rs mem) (HTL.State res m st asr asa)
-| match_returnstate :
-    forall v v' stack mem res (MF : match_frames stack res),
-      val_value_lessdef v v' ->
-      match_states (RTL.Returnstate stack v mem) (HTL.Returnstate res v')
+    match_states
+      (RTL.State sf f sp st rs mem)
+      (HTL.State res m st asr asa)
+| match_returnstate : forall v v' stack mem res
+    (MF : match_frames stack res),
+    val_value_lessdef v v' ->
+    match_states
+      (RTL.Returnstate stack v mem)
+      (HTL.Returnstate res v')
 | match_initial_call :
-    forall f m m0 (TF : tr_module f m),
-      match_states (RTL.Callstate nil (AST.Internal f) nil m0) (HTL.Callstate nil m nil).
+  forall f m m0 (TF : tr_module f m),
+    match_states
+      (RTL.Callstate nil (AST.Internal f) nil m0)
+      (HTL.Callstate nil m nil).
 \end{minted}
   \caption{\texttt{match\_states} predicate used to match an RTL state to the equivalent HTL state.}\label{fig:match_states}
 \end{figure}