diff options
| author | Maxime Dénès | 2017-04-27 17:10:10 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-04-27 17:10:10 +0200 |
| commit | 44c781d3087aab80e017a288be0e44a9a0ae76a0 (patch) | |
| tree | e46c221ea5f3c3e38a584ac6e03375b85fd2c5ad | |
| parent | 5af2e114e7390159d789c317dd83e564daa9c266 (diff) | |
| parent | 2fc235b0e00c028d2e91c696926ad339232d51e3 (diff) | |
Merge PR#585: 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. |