From 7c72fcced79e89eeeccfbe0f7b510423c8e060ef Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Tue, 29 Sep 2020 15:27:48 +0200 Subject: [PATCH] Break long line. --- theories/bi/plainly.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/theories/bi/plainly.v b/theories/bi/plainly.v index 95a1dd5c8..756dba593 100644 --- a/theories/bi/plainly.v +++ b/theories/bi/plainly.v @@ -648,4 +648,5 @@ Hint Immediate plain_persistent : typeclass_instances. [class_apply @impl_persistent] shelves the [BiPlainly] premise, making proof search for the other premises fail. See the proof of [coreP_persistent] for an example where it would fail with a regular [Instance].*) -Hint Extern 4 (Persistent _) => notypeclasses refine (impl_persistent _ _ _ _ _) : typeclass_instances. +Hint Extern 4 (Persistent _) => + notypeclasses refine (impl_persistent _ _ _ _ _) : typeclass_instances. -- GitLab