From 6e22698aa7b463bb0a45c8eed84a0e8cb2476fcf Mon Sep 17 00:00:00 2001
From: barras
Date: Mon, 1 Aug 2011 13:11:47 +0000
Subject: fixed bug 2580. Quick fix: copy emitcodes before patching it

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14376 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/cemitcodes.mli | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'kernel/cemitcodes.mli')

diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli
index 43cebb4748..287c393046 100644
--- a/kernel/cemitcodes.mli
+++ b/kernel/cemitcodes.mli
@@ -13,6 +13,8 @@ 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
@@ -35,5 +37,8 @@ val force : to_patch_substituted -> body_code
 
 val subst_to_patch_subst : Mod_subst.substitution -> to_patch_substituted -> to_patch_substituted
 
+val repr_body_code :
+  to_patch_substituted -> Mod_subst.substitution list option * body_code
+
 val to_memory : bytecodes * bytecodes * fv -> to_patch
                (** init code, fun code, fv *)
-- 
cgit v1.2.3