SharedMemory: formatting cleanup

This commit is contained in:
Adam Chlipala 2016-04-24 15:31:34 -04:00
parent 9f938e6ac1
commit 7675534511

View file

@ -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.