diff options
Diffstat (limited to 'kernel/cbytegen.ml')
| -rw-r--r-- | kernel/cbytegen.ml | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index ac46dc583..d5435f0c3 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -540,14 +540,12 @@ let rec compile_constr reloc c sz cont = match kind_of_term c with | Meta _ -> invalid_arg "Cbytegen.compile_constr : Meta" | Evar _ -> invalid_arg "Cbytegen.compile_constr : Evar" - | Proj (p,c) -> - (* compile_const reloc p [|c|] sz cont *) - let kn = Projection.constant p in - let cb = lookup_constant kn !global_env in - (* TODO: better representation of projections *) - let pb = Option.get cb.const_proj in - let args = Array.make pb.proj_npars mkProp in - compile_const reloc kn Univ.Instance.empty (Array.append args [|c|]) sz cont + | Proj (p,c) -> + let kn = Projection.constant p in + let cb = lookup_constant kn !global_env in + let pb = Option.get cb.const_proj in + let n = pb.proj_arg in + compile_constr reloc c sz (Kproj (n,kn) :: cont) | Cast(c,_,_) -> compile_constr reloc c sz cont |