diff options
| author | Guillaume Melquiond | 2014-04-22 17:16:47 +0200 |
|---|---|---|
| committer | Guillaume Melquiond | 2014-04-22 18:07:02 +0200 |
| commit | 923aa7e32c2e388dde1b6ae66c55d74d02bed2ab (patch) | |
| tree | 4ed325ab6df92e98c724d7fab1a8aa9859c4b48f /plugins/syntax | |
| parent | ae5668c90fddd66026293828114f17c0fb6d2b92 (diff) | |
Replace the proof of sig_forall_dec from Kaliszyk/O'Connor by the one from Coquelicot.
This change removes the need for excluded middle. It also greatly
simplifies the proof (no need for geometric series, limits, constructive
epsilon, and so on).
Diffstat (limited to 'plugins/syntax')
0 files changed, 0 insertions, 0 deletions