From 7891aa0b3314911afd49160c1d0992aa119cb11a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 17 Aug 2017 19:26:16 +0200
Subject: [PATCH] Also type classes for conjunction and unit.

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

diff --git a/theories/base.v b/theories/base.v
index a4d0099d..f1db1c83 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -35,6 +35,14 @@ Existing Class Or.
 Existing Instance Or_l | 9.
 Existing Instance Or_r | 10.
 
+Inductive And (P1 P2 : Type) := And_intro : P1 → P2 → And P1 P2.
+Existing Class And.
+Existing Instance And_intro.
+
+Inductive Unit := Unit_intro : Unit.
+Existing Class Unit.
+Existing Instance Unit_intro.
+
 (** 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