diff options
Diffstat (limited to 'kernel/nativecode.ml')
| -rw-r--r-- | kernel/nativecode.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index ada7ae737f..f56b6f83e7 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 = |