diff options
| author | Matthieu Sozeau | 2014-06-21 16:08:53 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-06-21 16:08:53 +0200 |
| commit | 9b3a234e4cf002292ca4a67e1b72daac463b4c46 (patch) | |
| tree | 0344ae5606294f9efcdbcbb8d5731c96554f9396 /kernel/type_errors.ml | |
| parent | cb38fe75f0f846a701b1a3fba8bf5fe1093ce79f (diff) | |
When discharging polymorphic definitions, we must take into account all
polymorphic variables of the section as they might incur universe constraints that
were used to typecheck the body of the definition, even if the variable
itself was not used. For "Monomorphic" variables, their constraints are already
always pushed to the global context. This fixes bug # 3330.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions