From 3211eec2d48450673e3f8327cf82fa3fa5df43ce Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 21 Dec 2020 14:05:05 +0100
Subject: [PATCH] option is non-expansive.

---
 theories/typing/lib/option.v | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/theories/typing/lib/option.v b/theories/typing/lib/option.v
index b7d0b2fd..4a1a153e 100644
--- a/theories/typing/lib/option.v
+++ b/theories/typing/lib/option.v
@@ -7,6 +7,12 @@ Section option.
 
   Definition option (τ : type) := Σ[unit; τ]%T.
 
+  Global Instance option_ne : NonExpansive option.
+  Proof. solve_proper. Qed.
+
+  Global Instance option_type_ne : TypeNonExpansive option.
+  Proof. solve_proper. Qed.
+
   (* Variant indices. *)
   Definition none := 0%nat.
   Definition some := 1%nat.
-- 
GitLab