Merge PR #8773: [checker] Refactor by sharing code with the kernel

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