From 2fc235b0e00c028d2e91c696926ad339232d51e3 Mon Sep 17 00:00:00 2001
From: Vadim Zaliva
Date: Wed, 26 Apr 2017 11:21:10 -0700
Subject: Small typo in comment

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

diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index f659c31f95..9ae9dde28d 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -223,7 +223,7 @@ Proof.
 Qed.
 
 (** [(IF_then_else P Q R)], written [IF P then Q else R] denotes
-    either [P] and [Q], or [~P] and [Q] *)
+    either [P] and [Q], or [~P] and [R] *)
 
 Definition IF_then_else (P Q R:Prop) := P /\ Q \/ ~ P /\ R.
 
-- 
cgit v1.2.3