diff options
Diffstat (limited to 'kernel/term_typing.ml')
| -rw-r--r-- | kernel/term_typing.ml | 20 |
1 files changed, 18 insertions, 2 deletions
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index a316b4492b..83e566041f 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -251,7 +251,24 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) match proj with | None -> compile_constant_body env def | Some pb -> - compile_constant_body env (Def (Mod_subst.from_val pb.proj_body)) + (* The compilation of primitive projections is a bit tricky, because + they refer to themselves (the body of p looks like fun c => + Proj(p,c)). We break the cycle by building an ad-hoc compilation + environment. A cleaner solution would be that kernel projections are + simply Proj(i,c) with i an int and c a constr, but we would have to + get rid of the compatibility layer. *) + let cb = + { const_hyps = hyps; + const_body = def; + const_type = typ; + const_proj = proj; + const_body_code = None; + const_polymorphic = poly; + const_universes = univs; + const_inline_code = inline_code } + in + let env = add_constant kn cb env in + compile_constant_body env def in Option.map Cemitcodes.from_val res in { const_hyps = hyps; @@ -263,7 +280,6 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) const_universes = univs; const_inline_code = inline_code } - (*s Global and local constant declaration. *) let translate_constant env kn ce = |