Merge PR #6965: [api] Move universe syntax to `Glob_term`

1 files changed, 9 insertions, 9 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index def8425ec3..48f15f8979 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)