diff options
Diffstat (limited to 'checker/inductive.mli')
-rw-r--r-- | checker/inductive.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/inductive.mli b/checker/inductive.mli index 8f605935d..0170bbc94 100644 --- a/checker/inductive.mli +++ b/checker/inductive.mli @@ -31,7 +31,7 @@ val type_of_inductive : env -> mind_specif puniverses -> constr (* Return type as quoted by the user *) val type_of_constructor : pconstructor -> mind_specif -> constr -val arities_of_specif : mutual_inductive puniverses -> mind_specif -> constr array +val arities_of_specif : MutInd.t puniverses -> mind_specif -> constr array (* [type_case_branches env (I,args) (p:A) c] computes useful types about the following Cases expression: |