better detection of nested recursion in Function

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

1 files changed, 11 insertions, 0 deletions

diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index b5f13270d7..fe6402db7d 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -172,12 +172,23 @@ let rank_for_arg_list h =
   | x::tl -> if predicate h x then Some i else rank_aux (i+1) tl in
   rank_aux 0;;
 
+let rec check_not_nested f t = 
+  match kind_of_term t with 
+    | App(g, _) when eq_constr f g -> 
+	errorlabstrm "recdef" (str "Nested recursive function are not allowed with Function")
+    | Var(_) when t = f -> errorlabstrm "recdef" (str "Nested recursive function are not allowed with Function")
+    | _ -> iter_constr (check_not_nested f) t 
+
+
+
+
 let rec (find_call_occs : int -> int -> constr -> constr ->
   (constr list -> constr) * constr list list) =
  fun nb_arg nb_lam f expr ->
   match (kind_of_term expr) with
     App (g, args) when g = f ->
       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");
+      Array.iter (check_not_nested f) args;
       (fun l -> List.hd l), [Array.to_list args]
   | App (g, args) ->
      let (largs: constr list) = Array.to_list args in