diff options
Diffstat (limited to 'pretyping/inductiveops.ml')
| -rw-r--r-- | pretyping/inductiveops.ml | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 34243f499c..913afb2191 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -331,6 +331,12 @@ let get_constructors env (ind,params) = Array.init (Array.length mip.mind_consnames) (fun j -> get_constructor (ind,mib,mip,params) (j+1)) +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 + | _ -> None + (* substitution in a signature *) let substnl_rel_context subst n sign = |