diff options
| author | Enrico Tassi | 2020-02-13 17:24:57 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2020-02-13 17:24:57 +0100 |
| commit | 6e020b001ec8b9d84293c5e9e7115bb1ddf901ca (patch) | |
| tree | 987e80de2abda3cb2b898e05d39db07d320c5edb /kernel/term.mli | |
| parent | eb83c142eb33de18e3bfdd7c32ecfb797a640c38 (diff) | |
| parent | b468bb9e7110be4e1a1c9b13da16720b64d1125e (diff) | |
Merge PR #11417: Move kind_of_type from the kernel to EConstr.
Reviewed-by: SkySkimmer
Reviewed-by: gares
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"] |