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

10 files changed, 30 insertions, 12 deletions

diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index b4e1a1b10..0ff6a330f 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -20,7 +20,6 @@ open EConstr
 open Vars
 open Pattern
 open Patternops
-open Misctypes
 open Context.Rel.Declaration
 open Ltac_pretype
 (*i*)
@@ -277,6 +276,7 @@ let matches_core env sigma allow_bound_rels
 
       | PSort ps, Sort s ->
 
+        let open Glob_term in
         begin match ps, ESorts.kind sigma s with
         | GProp, Prop Null -> subst
         | GSet, Prop Pos -> subst
diff --git a/pretyping/constrexpr.ml b/pretyping/constrexpr.ml
index fda31756a..1443dfb51 100644
--- a/pretyping/constrexpr.ml
+++ b/pretyping/constrexpr.ml
@@ -17,7 +17,7 @@ open Decl_kinds
 
 (** [constr_expr] is the abstract syntax tree produced by the parser *)
 
-type universe_decl_expr = (lident list, glob_constraint list) gen_universe_decl
+type universe_decl_expr = (lident list, Glob_term.glob_constraint list) gen_universe_decl
 
 type ident_decl = lident * universe_decl_expr option
 type name_decl = lname * universe_decl_expr option
@@ -50,7 +50,7 @@ type prim_token =
   | Numeral of raw_natural_number * sign
   | String of string
 
-type instance_expr = Misctypes.glob_level list
+type instance_expr = Glob_term.glob_level list
 
 type cases_pattern_expr_r =
   | CPatAlias of cases_pattern_expr * lname
@@ -98,7 +98,7 @@ and constr_expr_r =
   | CHole   of Evar_kinds.t option * intro_pattern_naming_expr * Genarg.raw_generic_argument option
   | CPatVar of patvar
   | CEvar   of Glob_term.existential_name * (Id.t * constr_expr) list
-  | CSort   of glob_sort
+  | CSort   of Glob_term.glob_sort
   | CCast   of constr_expr * constr_expr cast_type
   | CNotation of notation * constr_notation_substitution
   | CGeneralization of binding_kind * abstraction_kind option * constr_expr
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 817b8ba6e..5310455fe 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -14,7 +14,6 @@ open EConstr
 open Glob_term
 open Termops
 open Mod_subst
-open Misctypes
 open Evd
 open Ltac_pretype
 
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index 3c3f75a68..6ecb479e6 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -22,6 +22,25 @@ open Misctypes
 
 type existential_name = Id.t
 
+(** 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
+
 (**  The kind of patterns that occurs in "match ... with ... end"
 
      locs here refers to the ident's location, not whole pat *)
diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
index 0f0af5409..1b536bfda 100644
--- a/pretyping/miscops.ml
+++ b/pretyping/miscops.ml
@@ -29,7 +29,7 @@ let smartmap_cast_type f c =
 
 (** Equalities on [glob_sort] *)
 
-let glob_sort_eq g1 g2 = match g1, g2 with
+let glob_sort_eq g1 g2 = let open Glob_term in match g1, g2 with
 | GProp, GProp -> true
 | GSet, GSet -> true
 | GType l1, GType l2 ->
diff --git a/pretyping/miscops.mli b/pretyping/miscops.mli
index abe817fe5..1d4504541 100644
--- a/pretyping/miscops.mli
+++ b/pretyping/miscops.mli
@@ -18,7 +18,7 @@ val smartmap_cast_type : ('a -> 'a) -> 'a cast_type -> 'a cast_type
 
 (** Equalities on [glob_sort] *)
 
-val glob_sort_eq : glob_sort -> glob_sort -> bool
+val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool
 
 (** Equalities on [intro_pattern_naming] *)
 
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 7dd0954bc..996a2dc36 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -30,7 +30,7 @@ type constr_pattern =
   | PLambda of Name.t * constr_pattern * constr_pattern
   | PProd of Name.t * constr_pattern * constr_pattern
   | PLetIn of Name.t * constr_pattern * constr_pattern option * constr_pattern
-  | PSort of glob_sort
+  | PSort of Glob_term.glob_sort
   | PMeta of patvar option
   | PIf of constr_pattern * constr_pattern * constr_pattern
   | PCase of case_info_pattern * constr_pattern * constr_pattern *
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 35cc5702a..616ccf0cf 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -245,7 +245,7 @@ let interp_known_level_info ?loc evd = function
     with Not_found ->
       user_err ?loc ~hdr:"interp_known_level_info" (str "Undeclared universe " ++ Libnames.pr_reference ref)
 
-let interp_level_info ?loc evd : Misctypes.level_info -> _ = function
+let interp_level_info ?loc evd : level_info -> _ = function
   | UUnknown -> new_univ_level_variable ?loc univ_rigid evd
   | UAnonymous -> new_univ_level_variable ?loc univ_flexible evd
   | UNamed s -> interp_universe_level_name ~anon_rigidity:univ_flexible evd s
@@ -499,7 +499,7 @@ let interp_known_glob_level ?loc evd = function
   | GSet -> Univ.Level.set
   | GType s -> interp_known_level_info ?loc evd s
 
-let interp_glob_level ?loc evd : Misctypes.glob_level -> _ = function
+let interp_glob_level ?loc evd : glob_level -> _ = function
   | GProp -> evd, Univ.Level.prop
   | GSet -> evd, Univ.Level.set
   | GType s -> interp_level_info ?loc evd s
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 415c4e172..73f5b77e0 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -22,7 +22,7 @@ open Ltac_pretype
 open Evardefine
 
 val interp_known_glob_level : ?loc:Loc.t -> Evd.evar_map ->
-  Misctypes.glob_level -> Univ.Level.t
+  glob_level -> Univ.Level.t
 
 (** An auxiliary function for searching for fixpoint guard indexes *)
 
diff --git a/pretyping/vernacexpr.ml b/pretyping/vernacexpr.ml
index 3a49d6cf8..e15c3ad04 100644
--- a/pretyping/vernacexpr.ml
+++ b/pretyping/vernacexpr.ml
@@ -338,7 +338,7 @@ type nonrec vernac_expr =
   | VernacScheme of (lident option * scheme) list
   | VernacCombinedScheme of lident * lident list
   | VernacUniverse of lident list
-  | VernacConstraint of glob_constraint list
+  | VernacConstraint of Glob_term.glob_constraint list
 
   (* Gallina extensions *)
   | VernacBeginSection of lident