diff options
Diffstat (limited to 'kernel/indtypes.mli')
| -rw-r--r-- | kernel/indtypes.mli | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index cb09cfa827..a827c17683 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -34,6 +34,19 @@ type inductive_error = exception InductiveError of inductive_error +val infos_and_sort : env -> constr -> Univ.Universe.t + +val check_subtyping_arity_constructor : env -> (constr -> constr) -> types -> int -> bool -> unit + +val check_positivity : chkpos:bool -> + Names.MutInd.t -> + Environ.env -> + (Constr.constr, Constr.types) Context.Rel.pt -> + Declarations.recursivity_kind -> + ('a * Names.Id.t list * Constr.types array * + (('b, 'c) Context.Rel.pt * 'd)) + array -> Int.t * Declarations.recarg Rtree.t array + (** The following function does checks on inductive declarations. *) val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body |