diff options
Diffstat (limited to 'pretyping/nativenorm.ml')
| -rw-r--r-- | pretyping/nativenorm.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 4b8e0e096..16d003f67 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -123,7 +123,7 @@ let construct_of_constr_notnative const env tag (mind, _ as ind) u allargs = try if const then let ctyp = type_constructor mind mib u (mip.mind_nf_lc.(0)) params in - retroknowledge Retroknowledge.get_vm_decompile_constant_info env (mkInd ind) tag, ctyp + Retroknowledge.get_vm_decompile_constant_info env.retroknowledge (mkInd ind) tag, ctyp else raise Not_found with Not_found -> @@ -188,12 +188,13 @@ let branch_of_switch lvl ans bs = bs ci in Array.init (Array.length tbl) branch -let get_proj env ((mind, _n), i) = +let get_proj env ((mind, n), i) = let mib = Environ.lookup_mind mind env in match mib.mind_record with - | None | Some None -> + | NotRecord | FakeRecord -> CErrors.anomaly (Pp.strbrk "Return type is not a primitive record") - | Some (Some (_, projs, _)) -> + | PrimRecord info -> + let _, projs, _ = info.(n) in Projection.make projs.(i) true let rec nf_val env sigma v typ = |