diff options
Diffstat (limited to 'kernel/term.mli')
| -rw-r--r-- | kernel/term.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/term.mli b/kernel/term.mli index 2150f21ed1..7fa817bada 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -190,10 +190,10 @@ type ('constr, 'types) kind_of_type = val kind_of_type : types -> (constr, types) kind_of_type (* Deprecated *) -type sorts_family = Sorts.family = InProp | InSet | InType +type sorts_family = Sorts.family = InSProp | InProp | InSet | InType [@@ocaml.deprecated "Alias for Sorts.family"] type sorts = Sorts.t = private - | Prop | Set + | SProp | Prop | Set | Type of Univ.Universe.t (** Type *) [@@ocaml.deprecated "Alias for Sorts.t"] |