From badda32dac81c746f2c185d15540584d1b49e356 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 12 Nov 2020 20:48:29 +0100
Subject: [PATCH] Break super long line.
---
iris_heap_lang/proofmode.v | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/iris_heap_lang/proofmode.v b/iris_heap_lang/proofmode.v
index 8826570fa..46b122bfe 100644
--- a/iris_heap_lang/proofmode.v
+++ b/iris_heap_lang/proofmode.v
@@ -86,7 +86,8 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
unify e' efoc;
eapply (tac_wp_pure _ _ _ _ K e');
[iSolveTC (* PureExec *)
- |try solve_vals_compare_safe (* The pure condition for PureExec -- handles trivial goals, including [vals_compare_safe] *)
+ |try solve_vals_compare_safe (* The pure condition for PureExec --
+ handles trivial goals, including [vals_compare_safe] *)
|iSolveTC (* IntoLaters *)
|wp_finish (* new goal *)
])
--
GitLab