From 9a202d2d32452c7df002f2c3ebb88d4f338dc720 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 24 Jul 2021 10:32:28 +0200
Subject: [PATCH] Add some newlines.

---
 theories/base.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/theories/base.v b/theories/base.v
index 8b7a1218..ebd343af 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -719,6 +719,7 @@ Definition prod_relation {A B} (R1 : relation A) (R2 : relation B) :
 
 Section prod_relation.
   Context `{RA : relation A, RB : relation B}.
+
   Global Instance prod_relation_refl :
     Reflexive RA → Reflexive RB → Reflexive (prod_relation RA RB).
   Proof. firstorder eauto. Qed.
-- 
GitLab