*** empty log message ***

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6380 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 2 insertions, 20 deletions

diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index f1c662207..8e31f5976 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -257,7 +257,8 @@ let subst_patch s (ri,pos) =
   | Reloc_const sc -> (Reloc_const (subst_strcst s sc), pos)
   | Reloc_getglobal kn -> (Reloc_getglobal (subst_con s kn), pos)
 
-let subst_to_patch s (code,pl,fv) = code,List.map (subst_patch s) pl,fv
+let subst_to_patch s (code,pl,fv) = 
+  code,List.rev_map (subst_patch s) pl,fv
 
 type body_code =
   | BCdefined of bool * to_patch
@@ -300,22 +301,3 @@ let to_memory (init_code, fun_code, fv) =
 
 
 
-
-
-(* Code pour la machine virtuelle *)
-let mkAccu_code n =
-  init ();
-  out opMAKEACCU; out_int n;
-  let code = String.create !out_position in
-  String.unsafe_blit !out_buffer 0 code 0 !out_position; 
-  code
-
-let mkPopStop_code n =
-  init();
-  if n = 0 then out opSTOP
-  else (out opPOP; out_int n; out opSTOP);
-  let code = String.create !out_position in
-  String.unsafe_blit !out_buffer 0 code 0 !out_position; 
-  code
-
-