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 8e31f59761..cccb184433 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -255,7 +255,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_con s kn), pos) + | Reloc_getglobal kn -> (Reloc_getglobal (fst (subst_con s kn)), pos) let subst_to_patch s (code,pl,fv) = code,List.rev_map (subst_patch s) pl,fv @@ -267,7 +267,7 @@ type body_code = let subst_body_code s = function | BCdefined (b,tp) -> BCdefined (b,subst_to_patch s tp) - | BCallias kn -> BCallias (subst_con s kn) + | BCallias kn -> BCallias (fst (subst_con s kn)) | BCconstant -> BCconstant type to_patch_substituted = body_code substituted |