diff options
Diffstat (limited to 'pretyping/inductiveops.ml')
| -rw-r--r-- | pretyping/inductiveops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 24bf7cbc03..91072dce8c 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -334,7 +334,7 @@ let get_constructors env (ind,params) = let get_projections env (ind,params) = let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in match mib.mind_record with - | Some (projs, pbs) when Array.length projs > 0 -> Some projs + | Some (Some (id, projs, pbs)) -> Some projs | _ -> None (* substitution in a signature *) |