diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-29 13:04:22 +0100 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-29 13:11:38 +0100 |
commit | f970991baef49fa5903e6b7aeb6ac62f8cfdf822 (patch) | |
tree | 0b14bafe702a6219d960111148ff3a0cdc9e18e6 /kernel/cemitcodes.ml | |
parent | 4444f04cfdbe449d184ac1ce0a56eb484805364d (diff) | |
parent | 78378ba9a79b18a658828d7a110414ad18b9a732 (diff) |
Merge branch 'v8.5'
Diffstat (limited to 'kernel/cemitcodes.ml')
-rw-r--r-- | kernel/cemitcodes.ml | 25 |
1 files changed, 10 insertions, 15 deletions
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 4e64ed697..5ba93eda0 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -19,7 +19,7 @@ open Mod_subst type reloc_info = | Reloc_annot of annot_switch | Reloc_const of structured_constant - | Reloc_getglobal of pconstant + | Reloc_getglobal of Names.constant type patch = reloc_info * int @@ -135,11 +135,11 @@ let slot_for_const c = enter (Reloc_const c); out_int 0 -and slot_for_annot a = +let slot_for_annot a = enter (Reloc_annot a); out_int 0 -and slot_for_getglobal p = +let slot_for_getglobal p = enter (Reloc_getglobal p); out_int 0 @@ -198,7 +198,7 @@ let emit_instr = function Array.iter (out_label_with_orig org) lbl_bodies | Kgetglobal q -> out opGETGLOBAL; slot_for_getglobal q - | Kconst((Const_b0 i)) -> + | Kconst (Const_b0 i) -> if i >= 0 && i <= 3 then out (opCONST0 + i) else (out opCONSTINT; out_int i) @@ -315,10 +315,10 @@ type to_patch = emitcodes * (patch list) * fv (* Substitution *) let rec subst_strcst s sc = match sc with - | Const_sorts _ | Const_b0 _ -> sc + | Const_sorts _ | Const_b0 _ | Const_univ_level _ | Const_type _ -> 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,u) -> let kn,i = ind in Const_ind((subst_mind s kn, i), u) + | Const_ind ind -> let kn,i = ind in Const_ind (subst_mind s kn, i) let subst_patch s (ri,pos) = match ri with @@ -327,7 +327,7 @@ let subst_patch s (ri,pos) = 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 (subst_pcon s kn), pos) + | Reloc_getglobal kn -> (Reloc_getglobal (subst_constant s kn), pos) let subst_to_patch s (code,pl,fv) = code,List.rev_map (subst_patch s) pl,fv @@ -336,12 +336,12 @@ let subst_pconstant s (kn, u) = (fst (subst_con_kn s kn), u) type body_code = | BCdefined of to_patch - | BCalias of pconstant + | BCalias of Names.constant | BCconstant type to_patch_substituted = | PBCdefined of to_patch substituted -| PBCalias of pconstant substituted +| PBCalias of Names.constant substituted | PBCconstant let from_val = function @@ -351,7 +351,7 @@ let from_val = function let force = function | PBCdefined tp -> BCdefined (force subst_to_patch tp) -| PBCalias cu -> BCalias (force subst_pconstant cu) +| PBCalias cu -> BCalias (force subst_constant cu) | PBCconstant -> BCconstant let subst_to_patch_subst s = function @@ -383,8 +383,3 @@ let to_memory (init_code, fun_code, fv) = | Label_undefined patchlist -> assert (patchlist = []))) !label_table; (code, reloc, fv) - - - - - |