diff options
| author | Vadim Zaliva | 2017-04-26 11:21:10 -0700 |
|---|---|---|
| committer | GitHub | 2017-04-26 11:21:10 -0700 |
| commit | 2fc235b0e00c028d2e91c696926ad339232d51e3 (patch) | |
| tree | 5aac50c21c08138256f5800c6daf68357326a6ba | |
| parent | adc2035410a339cfa88dae527b631f5131adaa54 (diff) | |
Small typo in comment
| -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 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. |