diff options
Diffstat (limited to 'kernel/vmvalues.ml')
| -rw-r--r-- | kernel/vmvalues.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index 9a3eadf747..ac5350e9fa 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 @@ -335,10 +334,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 |