Erik de Castro Lopo writes:
 > with a no-recursive outer function and a tail recursive inner function.
 > It would still be nice to know if the inner function is tail recursive.

As  already explained by  Basile, the  right notion  is that  of "tail
call"  not of "tail  recursive function"  (you can  define it  as "all
recursive  calls  are tail  calls",  but  it  is less  precise).   For
instance, the following function
 
   let rec fold f s accu =
      match s with
        Empty -> accu
      | Node(l, v, r, _) -> fold f r (f v (fold f l accu))

has two recursive calls, one which is  not a tail call (fold f l accu)
and one which is (fold f r ...)

Being warned of non-tail calls may be useful in some situations, but I
guess the  issue is often the call  to a library function  that is not
tail recursive. That's  why you need the documentation  to be explicit
about that...

-- 
Jean-Christophe Filliâtre (http://www.lri.fr/~filliatr)