diff options
Diffstat (limited to 'kernel/term.ml')
| -rw-r--r-- | kernel/term.ml | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/kernel/term.ml b/kernel/term.ml index b44e038e9..4851a9c0d 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -16,14 +16,11 @@ open Vars open Constr (* Deprecated *) -type contents = Sorts.contents = Pos | Null -[@@ocaml.deprecated "Alias for Sorts.contents"] - type sorts_family = Sorts.family = InProp | InSet | InType [@@ocaml.deprecated "Alias for Sorts.family"] type sorts = Sorts.t = - | Prop of Sorts.contents (** Prop and Set *) + | Prop | Set | Type of Univ.Universe.t (** Type *) [@@ocaml.deprecated "Alias for Sorts.t"] @@ -339,7 +336,7 @@ let strip_lam_n n t = snd (decompose_lam_n n t) Such a term can canonically be seen as the pair of a context of types and of a sort *) -type arity = Context.Rel.t * Sorts.t +type arity = Constr.rel_context * Sorts.t let destArity = let open Context.Rel.Declaration in |