From 7675534511917009cadccea1198ed4409757b9d8 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Sun, 24 Apr 2016 15:31:34 -0400
Subject: [PATCH] SharedMemory: formatting cleanup

---
 SharedMemory.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/SharedMemory.v b/SharedMemory.v
index 4a88279..74d26fd 100644
--- a/SharedMemory.v
+++ b/SharedMemory.v
@@ -1748,14 +1748,14 @@ Theorem independent_threads_ok_again :
                (fun p => let '(_, _, c) := p in
                          notAboutToFail c = true).
 Proof.
-  (* We need to supply that summary when invoking the proof principle, though we
+  (* We need to supply the summary when invoking the proof principle, though we
    * could also have used Ltac to compute it automatically. *)
   eapply step_stepC with (cs := [(_, {| Reads := {0, 1};
                                         Writes := {1};
                                         Locks := {} |})]
                                   ++ [(_, {| Reads := {2};
-                                         Writes := {2};
-                                         Locks := {} |})]).
+                                             Writes := {2};
+                                             Locks := {} |})]).
   analyzer.
   analyzer.