From f33ed5473bea96cae30c6618f7c8db98805c680a Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Fri, 26 Apr 2019 11:39:09 +0200
Subject: [PATCH] Fix typo in doc

---
 theories/base.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/base.v b/theories/base.v
index 64ccf58b..86d98c17 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -65,7 +65,7 @@ Hint Extern 0 (TCNoBackTrack _) => constructor; apply _ : typeclass_instances.
 
 (* A conditional at the type class level. Note that [TCIf P Q R] is not the same
 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,
+establish [Q], 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) : Prop :=
-- 
GitLab