diff --git a/theories/base.v b/theories/base.v
index 8b7a1218882e577a4d6e5b6c5b83cabf2633f12d..ebd343af3c13822b4c63ff4cb55d2d2f063dea03 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.