From 6e22698aa7b463bb0a45c8eed84a0e8cb2476fcf Mon Sep 17 00:00:00 2001
From: barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>
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.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'kernel/cemitcodes.ml')

diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 277b343b2..1f00a70e7 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -307,6 +307,8 @@ let init () =
 
 type emitcodes = string
 
+let copy = String.copy
+
 let length = String.length
 
 type to_patch = emitcodes * (patch list) * fv
@@ -348,6 +350,8 @@ let force = force subst_body_code
 
 let subst_to_patch_subst = subst_substituted
 
+let repr_body_code = repr_substituted
+
 let to_memory (init_code, fun_code, fv) =
   init();
   emit init_code;
-- 
cgit v1.2.3