From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 kernel/cemitcodes.ml | 23 +++++++++++++++--------
 1 file changed, 15 insertions(+), 8 deletions(-)

(limited to 'kernel/cemitcodes.ml')

diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 14f4f27c..50f5607e 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -13,20 +13,22 @@
 (* Extension: Arnaud Spiwack (support for native arithmetic), May 2005 *)
 
 open Names
-open Term
+open Constr
+open Vmvalues
 open Cbytecodes
 open Copcodes
 open Mod_subst
 
 type emitcodes = String.t
 
-external tcode_of_code : Bytes.t -> int -> Vmvalues.tcode = "coq_tcode_of_code"
+external tcode_of_code : Bytes.t -> Vmvalues.tcode = "coq_tcode_of_code"
 
 (* Relocation information *)
 type reloc_info =
   | Reloc_annot of annot_switch
   | Reloc_const of structured_constant
   | Reloc_getglobal of Names.Constant.t
+  | Reloc_proj_name of Projection.Repr.t
 
 let eq_reloc_info r1 r2 = match r1, r2 with
 | Reloc_annot sw1, Reloc_annot sw2 -> eq_annot_switch sw1 sw2
@@ -35,6 +37,8 @@ let eq_reloc_info r1 r2 = match r1, r2 with
 | Reloc_const _, _ -> false
 | Reloc_getglobal c1, Reloc_getglobal c2 -> Constant.equal c1 c2
 | Reloc_getglobal _, _ -> false
+| Reloc_proj_name p1, Reloc_proj_name p2 -> Projection.Repr.equal p1 p2
+| Reloc_proj_name _, _ -> false
 
 let hash_reloc_info r =
   let open Hashset.Combine in
@@ -42,6 +46,7 @@ let hash_reloc_info r =
   | Reloc_annot sw -> combinesmall 1 (hash_annot_switch sw)
   | Reloc_const c -> combinesmall 2 (hash_structured_constant c)
   | Reloc_getglobal c -> combinesmall 3 (Constant.hash c)
+  | Reloc_proj_name p -> combinesmall 4 (Projection.Repr.hash p)
 
 module RelocTable = Hashtbl.Make(struct
   type t = reloc_info
@@ -82,7 +87,7 @@ let patch buff pl f =
   (** Order seems important here? *)
   let reloc = CArray.map (fun (r, pos) -> (f r, pos)) pl.reloc_infos in
   let buff = patch_int buff reloc in
-  tcode_of_code buff (Bytes.length buff)
+  tcode_of_code buff
 
 (* Buffering of bytecode *)
 
@@ -187,6 +192,9 @@ let slot_for_getglobal env p =
   enter env (Reloc_getglobal p);
   out_int env 0
 
+let slot_for_proj_name env p =
+  enter env (Reloc_proj_name p);
+  out_int env 0
 
 (* Emission of one instruction *)
 
@@ -277,7 +285,7 @@ let emit_instr env = function
       if n <= 1 then out env (opSETFIELD0+n)
       else (out env opSETFIELD;out_int env n)
   | Ksequence _ -> invalid_arg "Cemitcodes.emit_instr"
-  | Kproj (n,p) -> out env opPROJ; out_int env n; slot_for_const env (Const_proj p)
+  | Kproj p -> out env opPROJ; out_int env (Projection.Repr.arg p); slot_for_proj_name env p
   | Kensurestackcapacity size -> out env opENSURESTACKCAPACITY; out_int env size
   (* spiwack *)
   | Kbranch lbl -> out env opBRANCH; out_label env lbl
@@ -350,11 +358,9 @@ let rec emit env insns remaining = match insns with
 type to_patch = emitcodes * patches * fv
 
 (* Substitution *)
-let rec subst_strcst s sc =
+let subst_strcst s sc =
   match sc with
-  | Const_sort _ | Const_b0 _ | Const_univ_level _ -> sc
-  | Const_proj p -> Const_proj (subst_constant s p)
-  | Const_bn(tag,args) -> Const_bn(tag,Array.map (subst_strcst s) args)
+  | Const_sort _ | Const_b0 _ | Const_univ_level _ | Const_val _ -> sc
   | Const_ind ind -> let kn,i = ind in Const_ind (subst_mind s kn, i)
 
 let subst_reloc s ri =
@@ -365,6 +371,7 @@ let subst_reloc s ri =
       Reloc_annot {a with ci = ci}
   | Reloc_const sc -> Reloc_const (subst_strcst s sc)
   | Reloc_getglobal kn -> Reloc_getglobal (subst_constant s kn)
+  | Reloc_proj_name p -> Reloc_proj_name (subst_proj_repr s p)
 
 let subst_patches subst p =
   let infos = CArray.map (fun (r, pos) -> (subst_reloc subst r, pos)) p.reloc_infos in
-- 
cgit v1.2.3