From 17776cbd7149f214154370fc9713026616397862 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 9 Jun 2021 01:36:55 +0200
Subject: [PATCH] File structure tweak.

---
 theories/option.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/theories/option.v b/theories/option.v
index ff4bfd44..412cd5ce 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -121,12 +121,13 @@ Section setoids.
   Global Instance option_equivalence :
     Equivalence (≡@{A}) → Equivalence (≡@{option A}).
   Proof. apply _. Qed.
+  Global Instance option_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (option A).
+  Proof. intros x y; destruct 1; f_equal; by apply leibniz_equiv. Qed.
+
   Global Instance Some_proper : Proper ((≡) ==> (≡@{option A})) Some.
   Proof. by constructor. Qed.
   Global Instance Some_equiv_inj : Inj (≡) (≡@{option A}) Some.
   Proof. by inversion_clear 1. Qed.
-  Global Instance option_leibniz `{!LeibnizEquiv A} : LeibnizEquiv (option A).
-  Proof. intros x y; destruct 1; f_equal; by apply leibniz_equiv. Qed.
 
   Lemma equiv_None mx : mx ≡ None ↔ mx = None.
   Proof. split; [by inversion_clear 1|intros ->; constructor]. Qed.
-- 
GitLab