diff options
Diffstat (limited to 'kernel/indtypes.mli')
| -rw-r--r-- | kernel/indtypes.mli | 21 |
1 files changed, 12 insertions, 9 deletions
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 5a38172c2d..840e23ed69 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -34,16 +34,19 @@ type inductive_error = exception InductiveError of inductive_error -(** The following function does checks on inductive declarations. *) +val infos_and_sort : env -> constr -> Univ.Universe.t -val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body +val check_subtyping_arity_constructor : env -> (constr -> constr) -> types -> int -> bool -> unit -(** The following enforces a system compatible with the univalent model *) +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 -val enforce_indices_matter : unit -> unit -val is_indices_matter : unit -> bool +(** The following function does checks on inductive declarations. *) -val compute_projections : pinductive -> Id.t -> Id.t -> - int -> Context.Rel.t -> int array -> int array -> - Context.Rel.t -> Context.Rel.t -> - (Constant.t array * projection_body array) +val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body |