diff options
| author | Gaëtan Gilbert | 2018-11-19 18:18:26 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-01-21 13:22:47 +0100 |
| commit | 9c678306157b2c6199091709ef7bb067f724f80c (patch) | |
| tree | 28bbb08c4500676b2eca478323243d867cf27c15 /kernel/indtypes.mli | |
| parent | 70ce3e98991a96f9d7f181a4a6f5b250457f1245 (diff) | |
Refactor typechecking of inductive types
We split into smaller functions, use more specific types for universe
manipulation, and try to limit how much of the big tuple gets passed
to subroutines.
Diffstat (limited to 'kernel/indtypes.mli')
| -rw-r--r-- | kernel/indtypes.mli | 15 |
1 files changed, 2 insertions, 13 deletions
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 5e37df6976..7810c1723e 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -14,19 +14,7 @@ open Declarations open Environ open Entries -(** Inductive type checking and errors *) - -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. *) - +(** Check an inductive. *) val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body (** Deprecated *) @@ -41,6 +29,7 @@ type inductive_error = | NotAnArity of env * constr | BadEntry | LargeNonPropInductiveNotInType + | BadUnivs [@@ocaml.deprecated "Use [Type_errors.inductive_error]"] exception InductiveError of Type_errors.inductive_error |