From 1bbe31fef7b963cfbe92e59d5c763fbd0dd0b5b7 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 8 Aug 2017 22:23:47 +0200
Subject: [PATCH] Add Or type class.

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

diff --git a/theories/base.v b/theories/base.v
index 88031b3b..a4d0099d 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -25,6 +25,16 @@ Arguments unseal {_ _} _.
 Arguments seal_eq {_ _} _.
 Unset Primitive Projections.
 
+(* The [Or] class is useful for efficiency: instead of having two instances
+[P → Q1 → R] and [P → Q2 → R] we could have one instance [P → Or Q1 Q2 → R],
+which avoids the need to derive [P] twice. *)
+Inductive Or (P1 P2 : Type) :=
+  | Or_l : P1 → Or P1 P2
+  | Or_r : P2 → Or P1 P2.
+Existing Class Or.
+Existing Instance Or_l | 9.
+Existing Instance Or_r | 10.
+
 (** Throughout this development we use [C_scope] for all general purpose
 notations that do not belong to a more specific scope. *)
 Delimit Scope C_scope with C.
-- 
GitLab