From a47bd32c261aa1ba6e30ef1b4d08cfc2746ce20f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
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.
---
 interp/constrextern.mli |  1 -
 interp/constrintern.ml  | 18 +++++++++---------
 interp/declare.mli      |  2 +-
 3 files changed, 10 insertions(+), 11 deletions(-)

(limited to 'interp')

diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 6f5887ca2..73c108319 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -18,7 +18,6 @@ open Pattern
 open Constrexpr
 open Notation_term
 open Notation
-open Misctypes
 open Ltac_pretype
 
 (** Translation of pattern, cases pattern, glob_constr and term into syntax
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index def8425ec..48f15f897 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -980,17 +980,17 @@ let intern_reference ref =
   in
   Smartlocate.global_of_extended_global r
 
-let sort_info_of_level_info (info: Misctypes.level_info) : (Libnames.reference * int) option =
+let sort_info_of_level_info (info: level_info) : (Libnames.reference * int) option =
   match info with
-  | Misctypes.UAnonymous -> None
-  | Misctypes.UUnknown -> None
-  | Misctypes.UNamed id -> Some (id, 0)
+  | UAnonymous -> None
+  | UUnknown -> None
+  | UNamed id -> Some (id, 0)
 
-let glob_sort_of_level (level: Misctypes.glob_level) : Misctypes.glob_sort =
+let glob_sort_of_level (level: glob_level) : glob_sort =
   match level with
-  | Misctypes.GProp -> Misctypes.GProp
-  | Misctypes.GSet -> Misctypes.GSet
-  | Misctypes.GType info -> Misctypes.GType [sort_info_of_level_info info]
+  | GProp -> GProp
+  | GSet -> GSet
+  | GType info -> GType [sort_info_of_level_info info]
 
 (* Is it a global reference or a syntactic definition? *)
 let intern_qualid qid intern env ntnvars us args =
@@ -1024,7 +1024,7 @@ let intern_qualid qid intern env ntnvars us args =
           DAst.make ?loc @@ GApp (DAst.make ?loc:loc' @@ GRef (ref, us), arg)
         | _ -> err ()
         end
-      | Some [s], GSort (Misctypes.GType []) -> DAst.make ?loc @@ GSort (glob_sort_of_level s)
+      | Some [s], GSort (GType []) -> DAst.make ?loc @@ GSort (glob_sort_of_level s)
       | Some [_old_level], GSort _new_sort ->
         (* TODO: add old_level and new_sort to the error message *)
         user_err ?loc (str "Cannot change universe level of notation " ++ pr_qualid qid.v)
diff --git a/interp/declare.mli b/interp/declare.mli
index f8cffbb1e..de4d8346a 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -88,5 +88,5 @@ val declare_univ_binders : GlobRef.t -> Universes.universe_binders -> unit
 val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit
 
 val do_universe : polymorphic -> Misctypes.lident list -> unit
-val do_constraint : polymorphic -> (Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list ->
+val do_constraint : polymorphic -> (Glob_term.glob_level * Univ.constraint_type * Glob_term.glob_level) list ->
                     unit
-- 
cgit v1.2.3