Merge PR #8817: SProp: the definitionally proof irrelevant universe

Ack-by: JasonGross
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: mattam82

1 files changed, 3 insertions, 3 deletions

diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index 9a3eadf747..777a207013 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -8,7 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 open Names
-open Sorts
 open Univ
 open Constr
 
@@ -138,6 +137,7 @@ let hash_annot_switch asw =
 let pp_sort s =
   let open Sorts in
   match s with
+  | SProp -> Pp.str "SProp"
   | Prop -> Pp.str "Prop"
   | Set -> Pp.str "Set"
   | Type u -> Pp.(str "Type@{" ++ Univ.pr_uni u ++ str "}")
@@ -335,10 +335,10 @@ let rec whd_accu a stk =
         let args = Array.init (nargs args) (arg args) in
         let s = Obj.obj (Obj.field at 0) in
         begin match s with
-        | Type u ->
+        | Sorts.Type u ->
           let inst = Instance.of_array (Array.map uni_lvl_val args) in
           let u = Univ.subst_instance_universe inst u in
-          Vatom_stk (Asort (Type u), [])
+          Vatom_stk (Asort (Sorts.sort_of_univ u), [])
         | _ -> assert false
         end
      | _ -> assert false