diff options
Diffstat (limited to 'pretyping/inductiveops.ml')
| -rw-r--r-- | pretyping/inductiveops.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 3150ed63b5..727fd6f859 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -71,7 +71,6 @@ let substnl_ind_type l n = map_inductive_type (substnl l n) let mkAppliedInd (IndType ((ind,params), realargs)) = applist (mkInd ind,params@realargs) - (* Does not consider imbricated or mutually recursive types *) let mis_is_recursive_subset listind rarg = let rec one_is_rec rvec = @@ -125,6 +124,10 @@ let get_full_arity_sign env ind = let (mib,mip) = Inductive.lookup_mind_specif env ind in mip.mind_arity_ctxt +let nconstructors ind = + let (mib,mip) = Inductive.lookup_mind_specif (Global.env()) ind in + Array.length mip.mind_consnames + (* Length of arity (w/o local defs) *) let inductive_nargs env ind = |