diff options
Diffstat (limited to 'kernel/nativecode.ml')
| -rw-r--r-- | kernel/nativecode.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index bd659a471f..041751ecfe 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1923,7 +1923,8 @@ let rec compile_deps env sigma prefix ~interactive init t = comp_stack, (mind_updates, const_updates) | Construct (((mind,_),_),u) -> compile_mind_deps env prefix ~interactive init mind | Proj (p,c) -> - compile_deps env sigma prefix ~interactive init (mkApp (mkConst p, [|c|])) + let term = mkApp (mkConst (Projection.constant p), [|c|]) in + compile_deps env sigma prefix ~interactive init term | Case (ci, p, c, ac) -> let mind = fst ci.ci_ind in let init = compile_mind_deps env prefix ~interactive init mind in |