From ef89aa7b5ecc8007ba7af218b78c161f80907b78 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 2 Sep 2017 21:49:25 +0200
Subject: [PATCH] Put the type class logical connectives in Prop.

Before, we often had to insert awkward casts when using them. Also,
the generality of also having them on Type, is probably not useful.
---
 theories/base.v | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/theories/base.v b/theories/base.v
index 0e960783..dabf8bdb 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -28,20 +28,20 @@ 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 TCOr (P1 P2 : Type) :=
+Inductive TCOr (P1 P2 : Prop) : Prop :=
   | TCOr_l : P1 → TCOr P1 P2
   | TCOr_r : P2 → TCOr P1 P2.
 Existing Class TCOr.
 Existing Instance TCOr_l | 9.
 Existing Instance TCOr_r | 10.
 
-Inductive TCAnd (P1 P2 : Type) := TCAnd_intro : P1 → P2 → TCAnd P1 P2.
+Inductive TCAnd (P1 P2 : Prop) : Prop := TCAnd_intro : P1 → P2 → TCAnd P1 P2.
 Existing Class TCAnd.
 Existing Instance TCAnd_intro.
 
-Inductive TCUnit := TCUnit_intro : TCUnit.
-Existing Class TCUnit.
-Existing Instance TCUnit_intro.
+Inductive TCTrue : Prop := TCTrue_intro : TCTrue.
+Existing Class TCTrue.
+Existing Instance TCTrue_intro.
 
 (** Throughout this development we use [C_scope] for all general purpose
 notations that do not belong to a more specific scope. *)
-- 
GitLab