diff options
Diffstat (limited to 'kernel/sorts.mli')
| -rw-r--r-- | kernel/sorts.mli | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/kernel/sorts.mli b/kernel/sorts.mli index 1bbde260..cac6229b 100644 --- a/kernel/sorts.mli +++ b/kernel/sorts.mli @@ -10,13 +10,12 @@ (** {6 The sorts of CCI. } *) -type contents = Pos | Null - type family = InProp | InSet | InType type t = -| Prop of contents (** Prop and Set *) -| Type of Univ.Universe.t (** Type *) + | Prop + | Set + | Type of Univ.Universe.t val set : t val prop : t |