diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-08-01 13:11:47 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-08-01 13:11:47 +0000 |
| commit | 6e22698aa7b463bb0a45c8eed84a0e8cb2476fcf (patch) | |
| tree | 9353a4d28597a3477ae7ddff1129bdabbc5a5295 /kernel/cemitcodes.ml | |
| parent | 172ed0c8c5c66f22b17e07de792da41c3d925b77 (diff) | |
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
Diffstat (limited to 'kernel/cemitcodes.ml')
| -rw-r--r-- | kernel/cemitcodes.ml | 4 |
1 files changed, 4 insertions, 0 deletions
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; |