From af0a04b8e16c2554e0c747da6d625799b332f5fe Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Wed, 11 Oct 2017 19:41:23 +0200
Subject: Remove Sorts.contents

---
 kernel/term.mli | 5 +----
 1 file changed, 1 insertion(+), 4 deletions(-)

(limited to 'kernel/term.mli')

diff --git a/kernel/term.mli b/kernel/term.mli
index f651d1a58..4d340399d 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -190,13 +190,10 @@ type ('constr, 'types) kind_of_type =
 val kind_of_type : types -> (constr, types) kind_of_type
 
 (* 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"]
-- 
cgit v1.2.3