compatibility with POWERPC

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

1 files changed, 15 insertions, 17 deletions

diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 108dadbb7..40965d2f5 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -466,29 +466,27 @@ let compile env c =
   let reloc = empty () in
   let init_code = compile_constr reloc c 0 [Kstop] in
   let fv = List.rev (!(reloc.in_env).fv_rev) in
-  if Options.print_bytecodes() then 
-    (draw_instr init_code; draw_instr !fun_code);
   init_code,!fun_code, Array.of_list fv
 
-
 let compile_constant_body env body opaque boxed =
   if opaque then BCconstant
   else match body with
   | None -> BCconstant
   | Some sb ->
       let body = Declarations.force sb in
-      match kind_of_term body with
-      | Const kn' -> BCallias (get_allias env kn')
-      | Construct _ ->
-	  let res = compile env body in
-	  let to_patch = to_memory res in
-	  BCdefined (false,to_patch)
-
-      | _ -> 
-	  let res = compile env body in
-	  let to_patch = to_memory res in
-	  (*if Options.print_bytecodes() then 
-	    (let init,fun_code,_= res in
-	    draw_instr init; draw_instr fun_code);*)
-	  BCdefined (boxed && Options.boxed_definitions (),to_patch)
+      if boxed then
+	let res = compile env body in
+	let to_patch = to_memory res in
+	BCdefined(true, to_patch)
+      else
+	match kind_of_term body with
+	| Const kn' -> BCallias (get_allias env kn')
+	| Construct _ ->
+	    let res = compile env body in
+	    let to_patch = to_memory res in
+	    BCdefined (false, to_patch)
+	| _ -> 
+	    let res = compile env body in
+	    let to_patch = to_memory res in
+	    BCdefined (false, to_patch)