diff options
| author | Matthieu Sozeau | 2015-07-07 17:04:45 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-07-07 17:06:39 +0200 |
| commit | 7c7726a798caa6b506a727703de24d2bb5bb3956 (patch) | |
| tree | e65226bba40098323b59cf8294cf12c1a5bffe82 /kernel/nativelib.ml | |
| parent | 024a7ab20b06d82571c68c3d2ac32cb60fb0053a (diff) | |
Univs: bug fix.
Missing universe substitutions of mind_params_ctxt when typechecking
cases, which appeared only when let-ins were used.
Diffstat (limited to 'kernel/nativelib.ml')
0 files changed, 0 insertions, 0 deletions