Imported Upstream version 8.5~beta3+dfsg

1 files changed, 16 insertions, 19 deletions

diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 2535a64d..ef0c9af4 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
 
@@ -127,11 +127,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
 
@@ -190,7 +190,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)
@@ -225,6 +225,7 @@ let emit_instr = function
       if n <= 1 then out (opSETFIELD0+n)
       else (out opSETFIELD;out_int n)
   | Ksequence _ -> invalid_arg "Cemitcodes.emit_instr"
+  | Kproj (n,p) -> out opPROJ; out_int n; slot_for_const (Const_proj p)
   (* spiwack *)
   | Kbranch lbl -> out opBRANCH; out_label lbl
   | Kaddint31 -> out opADDINT31
@@ -306,9 +307,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
@@ -317,7 +319,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
@@ -326,36 +328,36 @@ let subst_pconstant s (kn, u) = (fst (subst_con_kn s kn), u)
 
 type body_code =
   | BCdefined of to_patch
-  | BCallias of pconstant
+  | BCalias of Names.constant
   | BCconstant
 
 type to_patch_substituted =
 | PBCdefined of to_patch substituted
-| PBCallias of pconstant substituted
+| PBCalias of Names.constant substituted
 | PBCconstant
 
 let from_val = function
 | BCdefined tp -> PBCdefined (from_val tp)
-| BCallias cu -> PBCallias (from_val cu)
+| BCalias cu -> PBCalias (from_val cu)
 | BCconstant -> PBCconstant
 
 let force = function
 | PBCdefined tp -> BCdefined (force subst_to_patch tp)
-| PBCallias cu -> BCallias (force subst_pconstant cu)
+| PBCalias cu -> BCalias (force subst_constant cu)
 | PBCconstant -> BCconstant
 
 let subst_to_patch_subst s = function
 | PBCdefined tp -> PBCdefined (subst_substituted s tp)
-| PBCallias cu -> PBCallias (subst_substituted s cu)
+| PBCalias cu -> PBCalias (subst_substituted s cu)
 | PBCconstant -> PBCconstant
 
 let repr_body_code = function
 | PBCdefined tp ->
   let (s, tp) = repr_substituted tp in
   (s, BCdefined tp)
-| PBCallias cu ->
+| PBCalias cu ->
   let (s, cu) = repr_substituted cu in
-  (s, BCallias cu)
+  (s, BCalias cu)
 | PBCconstant -> (None, BCconstant)
 
 let to_memory (init_code, fun_code, fv) =
@@ -371,8 +373,3 @@ let to_memory (init_code, fun_code, fv) =
     | Label_undefined patchlist ->
 	assert (patchlist = []))) !label_table;
   (code, reloc, fv)
-
-
-
-
-