diff options
Diffstat (limited to 'kernel/nativecode.ml')
| -rw-r--r-- | kernel/nativecode.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 34f26086af..3e9e5976af 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1409,7 +1409,6 @@ let rec compile_deps env prefix ~interactive init t = let cb = lookup_constant c env in let (_, (_, const_updates)) = init in if is_code_loaded ~interactive cb.const_native_name - || cb.const_inline_code || (Cmap_env.mem c const_updates) then init else @@ -1422,6 +1421,10 @@ let rec compile_deps env prefix ~interactive init t = let const_updates = Cmap_env.add c (cb.const_native_name, name) const_updates in comp_stack, (mind_updates, const_updates) | Construct ((mind,_),_) -> compile_mind_deps env prefix ~interactive init mind + | Case (ci, p, c, ac) -> + let mind = fst ci.ci_ind in + let init = compile_mind_deps env prefix ~interactive init mind in + fold_constr (compile_deps env prefix ~interactive) init t | _ -> fold_constr (compile_deps env prefix ~interactive) init t let compile_constant_field env prefix con (code, symb, (mupds, cupds)) cb = |