From a7b4c68403d7933a4ed54ec3571f206706884a88 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 20 Mar 2020 13:21:13 +0100
Subject: [PATCH] Fix bad line break.

---
 theories/proofmode/frame_instances.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/proofmode/frame_instances.v b/theories/proofmode/frame_instances.v
index f9c8cd921..696da901b 100644
--- a/theories/proofmode/frame_instances.v
+++ b/theories/proofmode/frame_instances.v
@@ -138,8 +138,8 @@ Global Instance frame_and p progress1 progress2 R P1 P2 Q1 Q2 Q' :
   MakeAnd Q1 Q2 Q' →
   Frame p R (P1 ∧ P2) Q' | 9.
 Proof.
-  rewrite /MaybeFrame /Frame /MakeAnd => <- <- _ <-. apply and_intro;
-  [rewrite and_elim_l|rewrite and_elim_r]; done.
+  rewrite /MaybeFrame /Frame /MakeAnd => <- <- _ <-.
+  apply and_intro; [rewrite and_elim_l|rewrite and_elim_r]; done.
 Qed.
 
 Global Instance make_or_true_l P : KnownLMakeOr True P True.
-- 
GitLab