diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-06-05 23:12:47 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-06-05 23:12:47 +0200 |
| commit | af902fa028f8ceb152d9add198e7dd490a4394ca (patch) | |
| tree | 002f7dde0d60cf865d5e643204827eee132299ee /pretyping | |
| parent | 1c67e29e735ab1e7bb121304f710ef48a23a8b9b (diff) | |
| parent | e1e7888ac4519f4b7470cc8469f9fd924514e352 (diff) | |
Merge PR #7679: Clean native compilation of primitive projections
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/nativenorm.ml | 16 |
1 files changed, 13 insertions, 3 deletions
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 3fce2f3c6..4b8e0e096 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -188,6 +188,14 @@ let branch_of_switch lvl ans bs = bs ci in Array.init (Array.length tbl) branch +let get_proj env ((mind, _n), i) = + let mib = Environ.lookup_mind mind env in + match mib.mind_record with + | None | Some None -> + CErrors.anomaly (Pp.strbrk "Return type is not a primitive record") + | Some (Some (_, projs, _)) -> + Projection.make projs.(i) true + let rec nf_val env sigma v typ = match kind_of_value v with | Vaccu accu -> nf_accu env sigma accu @@ -279,9 +287,10 @@ and nf_atom env sigma atom = let codom = nf_type env sigma (codom vn) in mkProd(n,dom,codom) | Ameta (mv,_) -> mkMeta mv - | Aproj(p,c) -> + | Aproj (p, c) -> let c = nf_accu env sigma c in - mkProj(Projection.make p true,c) + let p = get_proj env p in + mkProj(p, c) | _ -> fst (nf_atom_type env sigma atom) and nf_atom_type env sigma atom = @@ -357,7 +366,8 @@ and nf_atom_type env sigma atom = | Aproj(p,c) -> let c,tc = nf_accu_type env sigma c in let cj = make_judge c tc in - let uj = Typeops.judge_of_projection env (Projection.make p true) cj in + let p = get_proj env p in + let uj = Typeops.judge_of_projection env p cj in uj.uj_val, uj.uj_type |