From 57cd43543edfc8961038e2da734c6477ff5ae2bc Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 19 Dec 2002 14:14:53 +0000
Subject: suppression de l'archive cvs d'un bout de debug

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3462 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/extraction/mlutil.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index 172dce2ddb..145d700ccb 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -1087,16 +1087,17 @@ let manual_inline = function
    we are free to act (AutoInline is set)
    \end{itemize} *)
 
-let inline_test' r t = 
+(*i  DEBUG 
+  let inline_test' r t = 
   let b = inline_test t in 
   if b then msgnl (Printer.pr_global r); 
-  b
+  b i*)
 
 let inline r t = 
   not (to_keep r) (* The user DOES want to keep it *)
   && (to_inline r (* The user DOES want to inline it *) 
      || (auto_inline () && lang () <> Haskell 
-	 && (is_recursor r || manual_inline r || inline_test' r t)))
+	 && (is_recursor r || manual_inline r || inline_test t)))
 
 (*S Optimization. *)
 
-- 
cgit v1.2.3