diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-10-27 10:28:57 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-10-27 10:32:11 +0100 |
| commit | 6bb322f5ac542d12cf482b8bf02d2ee46c950a66 (patch) | |
| tree | ef6d684f393cfa9ee0163442c7215b7524f1d07c /theories/Logic/ChoiceFacts.v | |
| parent | a9630535a1bbbef0a91795a8136d67fc636a9a93 (diff) | |
Fix some typos.
Diffstat (limited to 'theories/Logic/ChoiceFacts.v')
| -rw-r--r-- | theories/Logic/ChoiceFacts.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index d8416b3e2..033ad1568 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -52,7 +52,7 @@ We let also - IPL^2 = 2nd-order functional minimal predicate logic (with ex. quant.) - IPL_2^2 = 2nd-order impredicative, 2nd-order functional minimal pred. logic (with ex. quant.) -with no prerequisite on the non-emptyness of domains +with no prerequisite on the non-emptiness of domains Table of contents @@ -96,7 +96,7 @@ Local Unset Intuition Negation Unfolding. (** Choice, reification and description schemes *) -(** We make them all polymorphic. most of them have existentials as conclusion +(** We make them all polymorphic. Most of them have existentials as conclusion so they require polymorphism otherwise their first application (e.g. to an existential in [Set]) will fix the level of [A]. *) @@ -340,7 +340,7 @@ Qed. (** We show that the guarded formulations of the axiom of choice are equivalent to their "omniscient" variant and comes from the non guarded - formulation in presence either of the independance of general premises + formulation in presence either of the independence of general premises or subset types (themselves derivable from subtypes thanks to proof- irrelevance) *) |