From 6c34b0598c93cb62f23e1fa32fab0c9aacb53274 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers
Date: Thu, 22 Feb 2018 21:16:32 +0100
Subject: [PATCH] Put `TCIf` in `Prop`.
---
theories/base.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/base.v b/theories/base.v
index 3185a02..81022e4 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.
--
2.24.1