diff options
| author | Matthieu Sozeau | 2015-01-13 05:51:36 +0530 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-01-13 05:51:36 +0530 |
| commit | 098781a2a1885a4f8768518a94b5026de9d375e6 (patch) | |
| tree | 711fd05e03101239048ef9e86c0132fee2f3bb21 /kernel | |
| parent | c60f40ccecf526b5c7ce5adfe5908fdac3f66771 (diff) | |
Fix bug when discharging universe constraints coming from variables
into monomorphic constants, which was still using the de Bruijn encoding
Bug revealed by discharging of hidden internal monomorphic definition in
otherwise polymorphic developments. Makes coqchk work on Hurkens again.
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/cooking.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 4435b6ca1d..be71bd7b41 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -236,7 +236,13 @@ let cook_constant env { from = cb; info } = proj_eta = etab, etat; proj_type = ty'; proj_body = c' } in - let univs = UContext.union abs_ctx univs in + let univs = + let abs' = + if cb.const_polymorphic then abs_ctx + else instantiate_univ_context abs_ctx + in + UContext.union abs' univs + in (body, typ, Option.map projection cb.const_proj, cb.const_polymorphic, univs, cb.const_inline_code, Some const_hyps) |