diff options
Diffstat (limited to 'kernel/vmvalues.ml')
| -rw-r--r-- | kernel/vmvalues.ml | 6 |
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 |