diff options
Diffstat (limited to 'kernel/cemitcodes.ml')
| -rw-r--r-- | kernel/cemitcodes.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 2b9ca425f..2de8ef2bf 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -320,16 +320,16 @@ let rec subst_strcst s sc = match sc with | Const_sorts _ | Const_b0 _ -> sc | Const_bn(tag,args) -> Const_bn(tag,Array.map (subst_strcst s) args) - | Const_ind(ind) -> let kn,i = ind in Const_ind((subst_ind s kn, i)) + | Const_ind(ind) -> let kn,i = ind in Const_ind((subst_mind s kn, i)) let subst_patch s (ri,pos) = match ri with | Reloc_annot a -> let (kn,i) = a.ci.ci_ind in - let ci = {a.ci with ci_ind = (subst_ind s kn,i)} in + let ci = {a.ci with ci_ind = (subst_mind s kn,i)} in (Reloc_annot {a with ci = ci},pos) | Reloc_const sc -> (Reloc_const (subst_strcst s sc), pos) - | Reloc_getglobal kn -> (Reloc_getglobal (fst (subst_con s kn)), pos) + | Reloc_getglobal kn -> (Reloc_getglobal (fst (subst_con_kn s kn)), pos) let subst_to_patch s (code,pl,fv) = code,List.rev_map (subst_patch s) pl,fv @@ -341,7 +341,7 @@ type body_code = let subst_body_code s = function | BCdefined tp -> BCdefined (subst_to_patch s tp) - | BCallias kn -> BCallias (fst (subst_con s kn)) + | BCallias kn -> BCallias (fst (subst_con_kn s kn)) | BCconstant -> BCconstant type to_patch_substituted = body_code substituted |