diff options
Diffstat (limited to 'checker/inductive.mli')
| -rw-r--r-- | checker/inductive.mli | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/checker/inductive.mli b/checker/inductive.mli index ed3a7b53..0ca0d14a 100644 --- a/checker/inductive.mli +++ b/checker/inductive.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (*i*) @@ -22,14 +24,16 @@ type mind_specif = mutual_inductive_body * one_inductive_body Raises [Not_found] if the inductive type is not found. *) val lookup_mind_specif : env -> inductive -> mind_specif -val inductive_instance : mutual_inductive_body -> Univ.universe_instance +val inductive_is_polymorphic : mutual_inductive_body -> bool + +val inductive_is_cumulative : mutual_inductive_body -> bool 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: |