diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-07-04 14:22:08 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-07-05 02:00:07 +0200 |
| commit | a51cce369b9c634a93120092d4c7685a242d55b1 (patch) | |
| tree | dd68ea8dadf86f9a6eb400839f515ed5b9cf8f95 /kernel/cbytegen.ml | |
| parent | 31c7542731a62f56bd60f443a84d68813f8780a8 (diff) | |
Fix handling of primitive projections in VM.
I'm pushing this patch now because the previous treatment of such projections
in the VM was already unsound. It should however be carefully reviewed.
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 |