Allowing Set to be part of universe expressions.

Conversely, Type existential variables now (explicitly) cover the Set
case.

Similarly for Prop and SProp.

5 files changed, 8 insertions, 8 deletions

diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 2295562a78..5bebf955ec 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -121,7 +121,7 @@ let mk_mltype_data sigma env assums arity indname =
 let rec check_anonymous_type ind =
   let open Glob_term in
     match DAst.get ind with
-    | GSort (GType UUnknown) -> true
+    | GSort (UAnonymous {rigid=true}) -> true
     | GProd ( _, _, _, e)
     | GLetIn (_, _, _, e)
     | GLambda (_, _, _, e)
@@ -495,7 +495,7 @@ let extract_params indl =
 let extract_inductive indl =
   List.map (fun ({CAst.v=indname},_,ar,lc) -> {
     ind_name = indname;
-    ind_arity = Option.cata (fun x -> x) (CAst.make @@ CSort (Glob_term.GType Glob_term.UUnknown)) ar;
+    ind_arity = Option.cata (fun x -> x) (CAst.make @@ CSort (Glob_term.UAnonymous {rigid=true})) ar;
     ind_lc = List.map (fun (_,({CAst.v=id},t)) -> (id,t)) lc
   }) indl
 
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 5eec8aed1e..a8d7b6f217 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -296,8 +296,8 @@ GRAMMAR EXTEND Gram
       | -> { NoInline } ] ]
   ;
   univ_constraint:
-    [ [ l = universe_level; ord = [ "<" -> { Univ.Lt } | "=" -> { Univ.Eq } | "<=" -> { Univ.Le } ];
-	r = universe_level -> { (l, ord, r) } ] ]
+    [ [ l = universe_name; ord = [ "<" -> { Univ.Lt } | "=" -> { Univ.Eq } | "<=" -> { Univ.Le } ];
+        r = universe_name -> { (l, ord, r) } ] ]
   ;
   univ_decl :
     [ [  "@{" ; l = LIST0 identref; ext = [ "+" -> { true } | -> { false } ];
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index e307c0c268..80e6c9d337 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -39,8 +39,8 @@ open Pputils
     pr_sep_com spc @@ pr_lconstr_expr env sigma
 
   let pr_uconstraint (l, d, r) =
-    pr_glob_level l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++
-      pr_glob_level r
+    pr_glob_sort_name l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++
+      pr_glob_sort_name r
 
   let pr_univ_name_list = function
     | None -> mt ()
diff --git a/vernac/record.ml b/vernac/record.ml
index ead9ed5c90..c8c482531a 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -125,7 +125,7 @@ let typecheck_params_and_fields finite def poly pl ps records =
        let env = EConstr.push_rel_context newps env0 in
        let poly =
          match t with
-         | { CAst.v = CSort (Glob_term.GType Glob_term.UUnknown) } -> true | _ -> false in
+         | { CAst.v = CSort (Glob_term.UAnonymous {rigid=true}) } -> true | _ -> false in
        let sigma, s = interp_type_evars ~program_mode:false env sigma ~impls:empty_internalization_env t in
        let sred = Reductionops.whd_allnolet env sigma s in
          (match EConstr.kind sigma sred with
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 22427621e6..2cd40ee63b 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -405,7 +405,7 @@ let universe_subgraph ?loc g univ =
   let open Univ in
   let sigma = Evd.from_env (Global.env()) in
   let univs_of q =
-    let q =  Glob_term.(GType (UNamed q)) in
+    let q =  Glob_term.(GType q) in
     (* this function has a nice error message for not found univs *)
     LSet.singleton (Pretyping.interp_known_glob_level ?loc sigma q)
   in