diff options
| author | Pierre-Marie Pédrot | 2020-01-17 13:40:10 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-02-02 19:30:04 +0100 |
| commit | 238b0cb82a1e66332131f10de79f4abe55d4b0b2 (patch) | |
| tree | 583532caeb28c940c01766f8a7578a90e7a55b0b /kernel/term.mli | |
| parent | 47c1730d4a7c02ba56d0292143f25772319dd98c (diff) | |
Move kind_of_type from the kernel to ssr.
It was virtually unused except in ssr, and there is no reason to clutter
the kernel with irrelevant code.
Fixes #9390: What is the purpose of the function "kind_of_type"?
Diffstat (limited to 'kernel/term.mli')
| -rw-r--r-- | kernel/term.mli | 11 |
1 files changed, 0 insertions, 11 deletions
diff --git a/kernel/term.mli b/kernel/term.mli index d2de4177ce..1fef54257a 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -181,17 +181,6 @@ val destArity : types -> arity (** Tell if a term has the form of an arity *) val isArity : types -> bool -(** {5 Kind of type} *) - -type ('constr, 'types) kind_of_type = - | SortType of Sorts.t - | CastType of 'types * 'types - | ProdType of Name.t Context.binder_annot * 'types * 'types - | LetInType of Name.t Context.binder_annot * 'constr * 'types * 'types - | AtomicType of 'constr * 'constr array - -val kind_of_type : types -> (constr, types) kind_of_type - (* Deprecated *) type sorts_family = Sorts.family = InSProp | InProp | InSet | InType [@@ocaml.deprecated "Alias for Sorts.family"] |