diff --git a/theories/base.v b/theories/base.v
index 0e96078346f0c02def6b80ec5631b3069816f540..dabf8bdb10b60c357bf596b4b7f4172025730626 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. *)