From c7be6d5a1e548fe1fdfc7b3fc248613bfb7fc613 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Sun, 25 Feb 2018 16:28:00 +0100 Subject: [VM] Unify Const_sorts and Const_type, and remove Vsort. This simplifies the representation of values, and brings it closer to the ones of the native compiler. --- kernel/cemitcodes.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'kernel/cemitcodes.ml') diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 856b0b465..32d5387b2 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -350,7 +350,7 @@ type to_patch = emitcodes * patches * fv (* Substitution *) let rec subst_strcst s sc = match sc with - | Const_sorts _ | Const_b0 _ | Const_univ_level _ | Const_type _ -> sc + | Const_sort _ | Const_b0 _ | Const_univ_level _ -> sc | Const_proj p -> Const_proj (subst_constant s p) | Const_bn(tag,args) -> Const_bn(tag,Array.map (subst_strcst s) args) | Const_ind ind -> let kn,i = ind in Const_ind (subst_mind s kn, i) -- cgit v1.2.3