From 286ab375eb8a56de0becd7600ca249c91667e1c7 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 9 Apr 2014 15:36:10 -0400
Subject: Fix exponential behavior in native compiler with retroknowledge.

---
 kernel/nativecode.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'kernel/nativecode.ml')

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 2cbe9cd22d..f38a2c3146 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1767,6 +1767,7 @@ let compile_constant env sigma prefix ~interactive con body =
   | Def t ->
       let t = Mod_subst.force_constr t in
       let code = lambda_of_constr env sigma t in
+      if !Flags.debug then Pp.msg_debug (Pp.str "Generated lambda code");
       let is_lazy = is_lazy prefix t in
       let code = if is_lazy then mk_lazy code else code in
       let name =
@@ -1775,9 +1776,11 @@ let compile_constant env sigma prefix ~interactive con body =
       in
       let l = con_label con in
       let auxdefs,code = compile_with_fv env sigma [] (Some l) code in
+      if !Flags.debug then Pp.msg_debug (Pp.str "Generated mllambda code");
       let code =
         optimize_stk (Glet(Gconstant ("",con),code)::auxdefs)
       in
+      if !Flags.debug then Pp.msg_debug (Pp.str "Optimized mllambda code");
       code, name
   | _ -> 
       let i = push_symbol (SymbConst con) in
-- 
cgit v1.2.3