diff --git a/heap_lang/par.v b/heap_lang/par.v
index be5fd50051a0c3f4003365cac4b497dcf22c20f0..9a707763d81f0bae95f6135edba1c196bb56b331 100644
--- a/heap_lang/par.v
+++ b/heap_lang/par.v
@@ -3,10 +3,11 @@ From heap_lang Require Import wp_tactics notation.
 Import uPred.
 
 Definition par : val :=
-  λ: "fs", let: "handle" := ^spawn (Fst '"fs") in
-           let: "v2" := Snd '"fs" #() in
-           let: "v1" := ^join '"handle" in
-           Pair '"v1" '"v2".
+  λ: "fs",
+    let: "handle" := ^spawn (Fst '"fs") in
+    let: "v2" := Snd '"fs" #() in
+    let: "v1" := ^join '"handle" in
+    Pair '"v1" '"v2".
 Notation Par e1 e2 := (^par (Pair (λ: <>, e1) (λ: <>, e2)))%E.
 Notation ParV e1 e2 := (par (Pair (λ: <>, e1) (λ: <>, e2)))%E.
 (* We want both par and par^ to print like this. *)
diff --git a/heap_lang/spawn.v b/heap_lang/spawn.v
index 3239d6b70bfd20ea2e72fb67ba2550e3a8ea2e0e..fce2af45716724f2bed17bbbf3457a32c9403228 100644
--- a/heap_lang/spawn.v
+++ b/heap_lang/spawn.v
@@ -4,11 +4,15 @@ From heap_lang Require Import wp_tactics notation.
 Import uPred.
 
 Definition spawn : val :=
-  λ: "f", let: "c" := ref (InjL #0) in
-          Fork ('"c" <- InjR ('"f" #())) ;; '"c".
+  λ: "f",
+    let: "c" := ref (InjL #0) in
+    Fork ('"c" <- InjR ('"f" #())) ;; '"c".
 Definition join : val :=
-  rec: "join" "c" := match: !'"c" with InjR "x" => '"x"
-                                     | InjL <>  => '"join" '"c" end.
+  rec: "join" "c" :=
+    match: !'"c" with
+      InjR "x" => '"x"
+    | InjL <>  => '"join" '"c"
+    end.
 
 (** The monoids we need. *)
 (* Not bundling heapG, as it may be shared with other users. *)