diff options
| author | Matthieu Sozeau | 2014-06-17 15:22:18 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-17 15:42:15 +0200 |
| commit | 362e81735b07f96cb87e1203328592fc394beaad (patch) | |
| tree | 2e6f9e9030f220ef5650d533690b73c3feba5dce /kernel/inductive.ml | |
| parent | 2b7bede68c213fbb884c773c073ba31a886f41f4 (diff) | |
- Fix the de Bruijn problem in check_projection for good :)
- Fix HoTT coq bug #80, implicit arguments with primitive projections were
wrongly automatically infered.
Diffstat (limited to 'kernel/inductive.ml')
0 files changed, 0 insertions, 0 deletions