diff options
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 58909ce01..a08184ed5 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -297,7 +297,7 @@ let elim_sorts (_,mip) = mip.mind_kelim let is_private (mib,_) = mib.mind_private = Some true let is_primitive_record (mib,_) = match mib.mind_record with - | Some (projs, _) when Array.length projs > 0 -> true + | Some (Some _) -> true | _ -> false let extended_rel_list n hyps = |