diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-01-26 16:56:34 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-01-26 16:56:34 +0100 |
commit | bb08c29807439697fa7c2045000dd3e17a9428b1 (patch) | |
tree | 9100a2dd5c2cb92ddd083cb052e236cdee6b9690 /theories/Logic/ClassicalFacts.v | |
parent | d55ac4014632489e3009a2a7351d018b3b2d27ac (diff) | |
parent | 164c6861860e6b52818c031f901ffeff91fca16a (diff) |
Merge tag 'upstream/8.5'
Upstream version 8.5
Diffstat (limited to 'theories/Logic/ClassicalFacts.v')
-rw-r--r-- | theories/Logic/ClassicalFacts.v | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v index 6f736e45..c947062a 100644 --- a/theories/Logic/ClassicalFacts.v +++ b/theories/Logic/ClassicalFacts.v @@ -1,7 +1,7 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -442,10 +442,10 @@ Section Proof_irrelevance_WEM_CC. Theorem wproof_irrelevance_cc : ~~(b1 = b2). Proof. intros h. - refine (let NB := exist (fun P=>~~P -> P) B _ in _). + unshelve (refine (let NB := exist (fun P=>~~P -> P) B _ in _)). { exact (fun _ => b1). } pose proof (NoRetractToNegativeProp.paradox NB p2b b2p (wp2p2 h) wp2p1) as paradox. - refine (let F := exist (fun P=>~~P->P) False _ in _). + unshelve (refine (let F := exist (fun P=>~~P->P) False _ in _)). { auto. } exact (paradox F). Qed. @@ -658,4 +658,3 @@ Proof. exists x; intro; exact Hx. exists x0; exact Hnot. Qed. - |