diff options
author | Vadim Zaliva <lord@crocodile.org> | 2017-04-26 11:21:10 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-04-26 11:21:10 -0700 |
commit | 2fc235b0e00c028d2e91c696926ad339232d51e3 (patch) | |
tree | 5aac50c21c08138256f5800c6daf68357326a6ba /theories | |
parent | adc2035410a339cfa88dae527b631f5131adaa54 (diff) |
Small typo in comment
Diffstat (limited to 'theories')
-rw-r--r-- | theories/Init/Logic.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index f659c31f9..9ae9dde28 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. |