diff options
| author |  jforest <jforest@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-05-04 13:30:48 +0000 |
|---|---|---|
| committer | jforest <jforest@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-05-04 13:30:48 +0000 |
| commit | 1b350172cd8448a30ac9a4167a16ca5aaac2b619 (patch) | |
| tree | 022254f77030c1ff7021b4d89c48733278ed2225 | |
| parent | 090403f8cc2f1fa0e8c98c86fd6559182258b009 (diff) | |
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
| -rw-r--r-- | plugins/funind/recdef.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 3cbe0a03c..cab78e82e 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 -> []), [] |