diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-04-29 12:02:52 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-04-29 12:02:52 +0000 |
| commit | ace8263ee9d05a684a81b7a1256b675b4085a7ca (patch) | |
| tree | 7109013530de199e80c9201dc243311c88bd324f /theories/Logic/Hurkens.v | |
| parent | a7593dbed5402e4e0992712d2087596544734360 (diff) | |
Blancs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3976 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Logic/Hurkens.v')
| -rw-r--r-- | theories/Logic/Hurkens.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v index 0cb2ef5da..74629fcca 100644 --- a/theories/Logic/Hurkens.v +++ b/theories/Logic/Hurkens.v @@ -29,7 +29,7 @@ Section Paradox. Variable bool : Prop. -Variable p2b : Prop -> bool. +Variable p2b : Prop -> bool. Variable b2p : bool -> Prop. Hypothesis p2p1 : (A:Prop)(b2p (p2b A))->A. Hypothesis p2p2 : (A:Prop)A->(b2p (p2b A)). |