diff options
| author | Amin Timany | 2017-05-27 09:44:38 +0200 |
|---|---|---|
| committer | Amin Timany | 2017-05-28 22:29:12 +0200 |
| commit | bde0f3038bffa660b0fc15084fb99bce42c7aa43 (patch) | |
| tree | e198656fe5f7ec9d5df2a5043c069ae958d5d4f3 /kernel/cbytecodes.ml | |
| parent | 1c74df16e7a539f21418ddb09419ff0106960789 (diff) | |
Fix a bug in checker
Universe constraints of the inductive types were not instantiated before being pushed on the environment. This commit fixes this bug.
Diffstat (limited to 'kernel/cbytecodes.ml')
0 files changed, 0 insertions, 0 deletions