diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-09-23 11:44:25 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-09-24 12:25:55 +0200 |
| commit | 507732b8541dea205e4e0288f81ea0eb58a7c253 (patch) | |
| tree | ca09e842bb44d0932db2be21ece09713a4772a7a /theories/Logic | |
| parent | 4ca7900108f5b6d713b8d1c34afab284423bae65 (diff) | |
Hurkens.v: show proofs in coqdoc.
Diffstat (limited to 'theories/Logic')
| -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 3111c7351..06c72a4cb 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 *) |