From ccf74b05a724f5f8e6f2005c23b06e64e458634a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 5 Mar 2016 21:40:29 +0100
Subject: [PATCH] Improve indentation.

---
 heap_lang/par.v   |  9 +++++----
 heap_lang/spawn.v | 12 ++++++++----
 2 files changed, 13 insertions(+), 8 deletions(-)

diff --git a/heap_lang/par.v b/heap_lang/par.v
index be5fd5005..9a707763d 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 3239d6b70..fce2af457 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. *)
-- 
GitLab