diff options
Diffstat (limited to 'pretyping/nativenorm.ml')
| -rw-r--r-- | pretyping/nativenorm.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 4b8e0e096..7319846fb 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -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 = |