From 1b350172cd8448a30ac9a4167a16ca5aaac2b619 Mon Sep 17 00:00:00 2001
From: jforest
Date: Tue, 4 May 2010 13:30:48 +0000
Subject: Correction of bug 2290 (removing stupid message)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12990 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/funind/recdef.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 3cbe0a03ce..cab78e82e7 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -180,7 +180,6 @@ let rec (find_call_occs : int -> int -> constr -> constr ->
       if Array.length args <> nb_arg then errorlabstrm "recdef" (str "Partial application of function " ++ Printer.pr_lconstr expr ++ str " in its body is not allowed while using Function");
       (fun l -> List.hd l), [Array.to_list args]
   | App (g, args) ->
-      msgnl (str "NB_ARGS " ++ int nb_arg ++ str " " ++ Printer.pr_lconstr g);
      let (largs: constr list) = Array.to_list args in
      let rec find_aux = function
 	 []    -> (fun x -> []), []
-- 
cgit v1.2.3