diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-01-13 05:51:36 +0530 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-01-13 05:51:36 +0530 |
| commit | 098781a2a1885a4f8768518a94b5026de9d375e6 (patch) | |
| tree | 711fd05e03101239048ef9e86c0132fee2f3bb21 | |
| 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.
| -rw-r--r-- | kernel/cooking.ml | 8 | ||||
| -rw-r--r-- | library/declare.ml | 1 |
2 files changed, 7 insertions, 2 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 4435b6ca1..be71bd7b4 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) diff --git a/library/declare.ml b/library/declare.ml index 8f0ce9eb2..7f42a747e 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -146,7 +146,6 @@ let discharged_hyps kn sechyps = let discharge_constant ((sp, kn), obj) = let con = constant_of_kn kn in - let from = Global.lookup_constant con in let modlist = replacement_context () in let hyps,subst,uctx = section_segment_of_constant con in |