diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-11-15 23:17:12 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-11-15 23:17:12 +0000 |
| commit | beca7a2c11d6521bd9eec7bb0eb5d77a345f99ef (patch) | |
| tree | ef154fd63c47a3dc2c8092051f539f126fdd982e /interp/notation.mli | |
| parent | ab388686675f65e796b0520f7e3de4cdfe48b9b1 (diff) | |
Isolating the ingredients of the proof of Prop<>Type (r15973). Seeing
it as a consequence of the derivability of Hurkens' paradox in the
presence of a retract from Type to Prop.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15977 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/notation.mli')
0 files changed, 0 insertions, 0 deletions