diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-10-27 07:21:09 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-10-27 07:21:09 +0100 |
| commit | 65c8d91cd4c11b8de44f0b23cd44a3303cd54d4e (patch) | |
| tree | 5b7c97dc58c1b453cd4ba0df838e5cd7a452e309 /theories/Logic | |
| parent | cc81b38185b6f558a6908f64cfaa7ee94131bf6c (diff) | |
Fix some typos in comments.
Diffstat (limited to 'theories/Logic')
| -rw-r--r-- | theories/Logic/Hurkens.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v index 34dc954ec..6896b2d57 100644 --- a/theories/Logic/Hurkens.v +++ b/theories/Logic/Hurkens.v @@ -116,7 +116,7 @@ Section Paradox. (** ** Axiomatisation of impredicative universes in a Martin-Löf style *) (** System U- has two impredicative universes. In the proof of the - paradox they are slightly asymetric (in particular the reduction + paradox they are slightly asymmetric (in particular the reduction rules of the small universe are not needed). Therefore, the axioms are duplicated allowing for a weaker requirement than the actual system U-. *) |