diff --git a/theories/base.v b/theories/base.v
index 3185a0237468a75e6ebe87b6ed9eb24f5259b069..81022e4e5b8efda7117ddd0a85491781afd0b60d 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -67,7 +67,7 @@ as [TCOr (TCAnd P Q) R]: the latter will backtrack to [R] if it fails to
 establish [R], i.e. does not have the behavior of a conditional. Furthermore,
 note that [TCOr (TCAnd P Q) (TCAnd (TCNot P) R)] would not work; we generally
 would not be able to prove the negation of [P]. *)
-Inductive TCIf (P Q R : Prop) :=
+Inductive TCIf (P Q R : Prop) : Prop :=
   | TCIf_true : P → Q → TCIf P Q R
   | TCIf_false : R → TCIf P Q R.
 Existing Class TCIf.