From 56925d60207f940ebb88d56981f8cdff41c58247 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 25 Jun 2015 13:56:14 +0200
Subject: Exporting a purely functional interface to bytecode patching.

---
 kernel/cemitcodes.mli | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'kernel/cemitcodes.mli')

diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli
index 54b92b9121..398b60eca5 100644
--- a/kernel/cemitcodes.mli
+++ b/kernel/cemitcodes.mli
@@ -13,11 +13,9 @@ val subst_patch : Mod_subst.substitution -> patch -> patch
 
 type emitcodes
 
-val copy : emitcodes -> emitcodes
-
 val length : emitcodes -> int
 
-val patch_int : emitcodes -> (*pos*)int -> int -> unit
+val patch_int : emitcodes -> ((*pos*)int * int) list -> emitcodes
 
 type to_patch = emitcodes * (patch list) * fv
 
-- 
cgit v1.2.3


From 7d9331a2a188842a98936278d02177f1a6fa7001 Mon Sep 17 00:00:00 2001
From: Gregory Malecha
Date: Sat, 17 Oct 2015 21:40:49 -0700
Subject: Adds support for the virtual machine to perform reduction of universe
 polymorphic definitions.

- This implementation passes universes in separate arguments and does not
  eagerly instanitate polymorphic definitions.
- This means that it pays no cost on monomorphic definitions.
---
 kernel/cemitcodes.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/cemitcodes.mli')

diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli
index 54b92b9121..10f3a6087a 100644
--- a/kernel/cemitcodes.mli
+++ b/kernel/cemitcodes.mli
@@ -4,7 +4,7 @@ open Cbytecodes
 type reloc_info =
   | Reloc_annot of annot_switch
   | Reloc_const of structured_constant
-  | Reloc_getglobal of constant Univ.puniverses
+  | Reloc_getglobal of constant
 
 type patch = reloc_info * int
 
@@ -25,7 +25,7 @@ val subst_to_patch : Mod_subst.substitution -> to_patch -> to_patch
 
 type body_code =
   | BCdefined of to_patch
-  | BCalias of constant Univ.puniverses
+  | BCalias of constant
   | BCconstant
 
 
-- 
cgit v1.2.3