diff options
Diffstat (limited to 'kernel/cemitcodes.ml')
| -rw-r--r-- | kernel/cemitcodes.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 4219491631..1b93dc4b6a 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -254,7 +254,7 @@ let subst_patch s (ri,pos) = let ci = {a.ci with ci_ind = (subst_kn 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 (subst_kn s kn), pos) + | Reloc_getglobal kn -> (Reloc_getglobal (subst_con s kn), pos) let subst_to_patch s (code,pl,fv) = code,List.map (subst_patch s) pl,fv @@ -265,7 +265,7 @@ type body_code = let subst_body_code s = function | BCdefined (b,tp) -> BCdefined (b,subst_to_patch s tp) - | BCallias kn -> BCallias (subst_kn s kn) + | BCallias kn -> BCallias (subst_con s kn) | BCconstant -> BCconstant type to_patch_substituted = body_code substituted |