diff options
| author | mdenes | 2013-03-25 09:32:39 +0000 |
|---|---|---|
| committer | mdenes | 2013-03-25 09:32:39 +0000 |
| commit | 8a13513d5214a91f8bd9b7611675c400ee41a9f3 (patch) | |
| tree | 02a4c0185dfbd6caefa33ced43da869f77954745 /kernel | |
| parent | 39f62b3ecf3e5dcadd16b10a81c495a30bd24251 (diff) | |
Native compiler: Inlined constants are now compiled, fixing a bug reported by
Chantal Keller.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16356 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -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 = |