From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 theories/Logic/Hurkens.v | 25 +++++++++++--------------
 1 file changed, 11 insertions(+), 14 deletions(-)

(limited to 'theories/Logic/Hurkens.v')

diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v
index 841f843c..6c4a8533 100644
--- a/theories/Logic/Hurkens.v
+++ b/theories/Logic/Hurkens.v
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 (*                              Hurkens.v                               *)
 (************************************************************************)
@@ -360,13 +362,12 @@ Module NoRetractToModalProposition.
 Section Paradox.
 
 Variable M : Prop -> Prop.
-Hypothesis unit : forall A:Prop, A -> M A.
-Hypothesis join : forall A:Prop, M (M A) -> M A.
 Hypothesis incr : forall A B:Prop, (A->B) -> M A -> M B.
 
 Lemma strength: forall A (P:A->Prop), M(forall x:A,P x) -> forall x:A,M(P x).
 Proof.
-  eauto.
+  intros A P h x.
+  eapply incr in h; eauto.
 Qed.
 
 (** ** The universe of modal propositions *)
@@ -470,7 +471,7 @@ Hypothesis p2p2 : forall A:NProp, El A -> El (b2p (p2b A)).
 Theorem paradox : forall B:NProp, El B.
 Proof.
   intros B.
-  unshelve (refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _ _ _))).
+  unshelve (refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _))).
   + exact (fun P => ~~P).
   + exact bool.
   + exact p2b.
@@ -480,8 +481,6 @@ Proof.
   + cbn. auto.
   + cbn. auto.
   + cbn. auto.
-  + auto.
-  + auto.
 Qed.
 
 End Paradox.
@@ -516,7 +515,7 @@ Hypothesis p2p2 : forall A:NProp, El A -> El (b2p (p2b A)).
 Theorem mparadox : forall B:NProp, El B.
 Proof.
   intros B.
-  unshelve (refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _ _ _))).
+  unshelve (refine ((fun h => _) (NoRetractToModalProposition.paradox _ _ _ _ _ _ _ _))).
   + exact (fun P => P).
   + exact bool.
   + exact p2b.
@@ -526,8 +525,6 @@ Proof.
   + cbn. auto.
   + cbn. auto.
   + cbn. auto.
-  + auto.
-  + auto.
 Qed.
 
 End MParadox.
@@ -562,7 +559,7 @@ End Paradox.
 End NoRetractFromSmallPropositionToProp.
 
 
-(** * Large universes are no retracts of [Prop]. *)
+(** * Large universes are not retracts of [Prop]. *)
 
 (** The existence in the Calculus of Constructions with universes of a
     retract from some [Type] universe into [Prop] is inconsistent. *)
-- 
cgit v1.2.3