diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/inductiveops.ml | 5 | ||||
| -rw-r--r-- | pretyping/inductiveops.mli | 2 |
2 files changed, 6 insertions, 1 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 3150ed63b..727fd6f85 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 = diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index cc1bb7f41..cea769955 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -58,6 +58,8 @@ val mis_nf_constructor_type : val mis_constr_nargs : inductive -> int array val mis_constr_nargs_env : env -> inductive -> int array +val nconstructors : inductive -> int + (* Return the lengths of parameters signature and real arguments signature *) val inductive_nargs : env -> inductive -> int * int |