From 48a6ce6e7cbdc2a03767c61696425cd5d5827f4f Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Mon, 8 Jun 2015 22:34:07 +0200 Subject: Fix native compilation of primitive projections. Closes #4210. --- kernel/nativecode.ml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) (limited to 'kernel') diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index ada7ae737..f56b6f83e 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -2015,9 +2015,13 @@ let rec compile_deps env sigma prefix ~interactive init t = || (Cmap_env.mem c const_updates) then init else - let comp_stack, (mind_updates, const_updates) = match cb.const_body with - | Def t -> + let comp_stack, (mind_updates, const_updates) = + match cb.const_proj, cb.const_body with + | None, Def t -> compile_deps env sigma prefix ~interactive init (Mod_subst.force_constr t) + | Some pb, _ -> + let mind = pb.proj_ind in + compile_mind_deps env prefix ~interactive init mind | _ -> init in let code, name = -- cgit v1.2.3