diff options
| author | Maxime Dénès | 2014-03-12 10:46:49 -0400 |
|---|---|---|
| committer | Maxime Dénès | 2014-07-22 17:52:08 -0400 |
| commit | e0c70fc7cd8333a48a4bac47bcb0e01e4b737718 (patch) | |
| tree | 54419590bb77ed885e50cee0f2955dddeb7ba4fa /kernel/type_errors.ml | |
| parent | 9c9f5a3bde48a46c8e5146093392883ee16bc9e2 (diff) | |
Fixed proof of irrelevance of le on nat, inspired by the
corresponding proof in ssreflect.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions