Allowing Set to be part of universe expressions.

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

Similarly for Prop and SProp.

4 files changed, 16 insertions, 20 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index c05af8be45..701c07dc8d 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -758,8 +758,9 @@ let extended_glob_local_binder_of_decl ?loc u = DAst.make ?loc (extended_glob_lo
 
 let extern_glob_sort = function
   (* In case we print a glob_constr w/o having passed through detyping *)
-  | GType _ when not !print_universes -> GType UUnknown
-  | u -> u
+  | UNamed [(GSProp,0) | (GProp,0) | (GSet,0)] as u -> u
+  | UNamed _ when not !print_universes -> UAnonymous {rigid=true}
+  | UNamed _ | UAnonymous _ as u -> u
 
 let extern_universes = function
   | Some _ as l when !print_universes -> l
@@ -1310,10 +1311,10 @@ let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
           Array.map (fun (bl,_,_) -> bl) v,
           Array.map (fun (_,_,ty) -> ty) v,
           Array.map (fun (_,bd,_) -> bd) v)
-  | PSort Sorts.InSProp -> GSort GSProp
-  | PSort Sorts.InProp -> GSort GProp
-  | PSort Sorts.InSet -> GSort GSet
-  | PSort Sorts.InType -> GSort (GType UUnknown)
+  | PSort Sorts.InSProp -> GSort (UNamed [GSProp,0])
+  | PSort Sorts.InProp -> GSort (UNamed [GProp,0])
+  | PSort Sorts.InSet -> GSort (UNamed [GSet,0])
+  | PSort Sorts.InType -> GSort (UAnonymous {rigid=true})
   | PInt i -> GInt i
 
 let extern_constr_pattern env sigma pat =
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index b4294b4ff8..1a81dc41a1 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -998,18 +998,10 @@ let intern_reference qid =
   in
   Smartlocate.global_of_extended_global r
 
-let sort_info_of_level_info (info: level_info) : sort_info =
-  match info with
-  | UAnonymous -> UAnonymous
-  | UUnknown -> UUnknown
-  | UNamed id -> UNamed [id,0]
-
 let glob_sort_of_level (level: glob_level) : glob_sort =
   match level with
-  | GSProp -> GSProp
-  | GProp -> GProp
-  | GSet -> GSet
-  | GType info -> GType (sort_info_of_level_info info)
+  | UAnonymous {rigid} -> UAnonymous {rigid}
+  | UNamed id -> UNamed [id,0]
 
 (* Is it a global reference or a syntactic definition? *)
 let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args =
@@ -1045,7 +1037,7 @@ let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args =
           DAst.make ?loc @@ GApp (DAst.make ?loc:loc' @@ GRef (ref, us), arg)
         | _ -> err ()
         end
-      | Some [s], GSort (GType UUnknown) -> DAst.make ?loc @@ GSort (glob_sort_of_level s)
+      | Some [s], GSort (UAnonymous {rigid=true}) -> 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)
diff --git a/interp/declare.mli b/interp/declare.mli
index 795d9a767d..0b1a396a34 100644
--- a/interp/declare.mli
+++ b/interp/declare.mli
@@ -90,5 +90,4 @@ val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit
 val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit
 
 val do_universe : polymorphic -> lident list -> unit
-val do_constraint : polymorphic -> (Glob_term.glob_level * Univ.constraint_type * Glob_term.glob_level) list ->
-                    unit
+val do_constraint : polymorphic -> Glob_term.glob_constraint list -> unit
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 7f084fffdd..08619d912e 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -1190,7 +1190,11 @@ let rec match_ inner u alp metas sigma a1 a2 =
       Array.fold_left2 (match_in u alp metas) sigma bl1 bl2
   | GCast(t1, c1), NCast(t2, c2) ->
     match_cast (match_in u alp metas) (match_in u alp metas sigma t1 t2) c1 c2
-  | GSort (GType _), NSort (GType _) when not u -> sigma
+
+  (* Next pair of lines useful only if not coming from detyping *)
+  | GSort (UNamed [(GProp|GSet),0]), NSort (UAnonymous _) -> raise No_match
+  | GSort _, NSort (UAnonymous _) when not u -> sigma
+
   | GSort s1, NSort s2 when glob_sort_eq s1 s2 -> sigma
   | GInt i1, NInt i2 when Uint63.equal i1 i2 -> sigma
   | GPatVar _, NHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match