From 507732b8541dea205e4e0288f81ea0eb58a7c253 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Tue, 23 Sep 2014 11:44:25 +0200
Subject: Hurkens.v: show proofs in coqdoc.

---
 theories/Logic/Hurkens.v | 4 ++++
 1 file changed, 4 insertions(+)

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 *)
-- 
cgit v1.2.3