diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-06-08 22:34:07 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-06-08 22:34:07 +0200 |
| commit | 48a6ce6e7cbdc2a03767c61696425cd5d5827f4f (patch) | |
| tree | 5176c88991d0c15162533c80cd7a0c03f3d6200c /kernel/nativecode.ml | |
| parent | 1ef197db161f49de5c9b0900de1114c8b6750625 (diff) | |
Fix native compilation of primitive projections. Closes #4210.
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 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 = |