diff options
Diffstat (limited to 'kernel/cemitcodes.ml')
| -rw-r--r-- | kernel/cemitcodes.ml | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 1138031c7..277b343b2 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -331,12 +331,12 @@ let subst_to_patch s (code,pl,fv) = code,List.rev_map (subst_patch s) pl,fv type body_code = - | BCdefined of bool * to_patch + | BCdefined of to_patch | BCallias of constant | BCconstant let subst_body_code s = function - | BCdefined (b,tp) -> BCdefined (b,subst_to_patch s tp) + | BCdefined tp -> BCdefined (subst_to_patch s tp) | BCallias kn -> BCallias (fst (subst_con s kn)) | BCconstant -> BCconstant @@ -348,11 +348,6 @@ let force = force subst_body_code let subst_to_patch_subst = subst_substituted -let is_boxed tps = - match force tps with - | BCdefined(b,_) -> b - | _ -> false - let to_memory (init_code, fun_code, fv) = init(); emit init_code; |