From a47bd32c261aa1ba6e30ef1b4d08cfc2746ce20f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 24 Apr 2018 03:26:40 +0200
Subject: [api] Move universe syntax to `Glob_term`

We move syntax for universes from `Misctypes` to `Glob_term`. There is
basically no reason that this type is there instead of the proper
file, as witnessed by the diff.

Unfortunately the change is not compatible due to moving a type to a
higher level in the hierarchy, but we expect few problems.

This change plus the related PR (#6515) moving universe declaration to
their proper place make `Misctypes` into basically an empty file save
for introduction patterns.
---
 library/misctypes.ml | 19 -------------------
 1 file changed, 19 deletions(-)

(limited to 'library')

diff --git a/library/misctypes.ml b/library/misctypes.ml
index 72db3b31cb..b5d30559d8 100644
--- a/library/misctypes.ml
+++ b/library/misctypes.ml
@@ -50,25 +50,6 @@ type 'id move_location =
   | MoveFirst
   | MoveLast (** can be seen as "no move" when doing intro *)
 
-(** Sorts *)
-
-type 'a glob_sort_gen =
-  | GProp (** representation of [Prop] literal *)
-  | GSet  (** representation of [Set] literal *)
-  | GType of 'a (** representation of [Type] literal *)
-
-type 'a universe_kind =
-  | UAnonymous
-  | UUnknown
-  | UNamed of 'a
-
-type level_info = Libnames.reference universe_kind
-type glob_level = level_info glob_sort_gen
-type glob_constraint = glob_level * Univ.constraint_type * glob_level
-
-type sort_info = (Libnames.reference * int) option list
-type glob_sort = sort_info glob_sort_gen
-
 (** A synonym of [Evar.t], also defined in Term *)
 
 type existential_key = Evar.t
-- 
cgit v1.2.3