diff options
| -rw-r--r-- | theories/Logic/Hurkens.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v index 3111c73513..06c72a4cb0 100644 --- a/theories/Logic/Hurkens.v +++ b/theories/Logic/Hurkens.v @@ -59,6 +59,8 @@ Set Universe Polymorphism. +(* begin show *) + (** * A modular proof of Hurkens's paradox. *) (** It relies on an axiomatisation of a shallow embedding of system U- @@ -527,3 +529,5 @@ Proof. Qed. End PropNeqType. + +(* end show *) |