diff options
| author | Hugo Herbelin | 2014-07-15 18:15:26 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-07-15 18:15:52 +0200 |
| commit | c236b51348d2a39d8f105ef0c4e8a53fabc6e285 (patch) | |
| tree | 402fb6cf168c8f450c0efe44351a9d7519e22e92 /kernel/type_errors.ml | |
| parent | 6afdf9bd419e0353924789c6c0d5d92ecdae2f46 (diff) | |
Added a (constructive) proof of Weak Konig's lemma for decidable trees.
Renamed Fan.v into WeakFan.v since this was a proof of Weak Fan Theorem
after all.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions