If a fixpoint is not written with an explicit { struct ... }, then

all arguments are tried successively (from left to right) until one is 
found that satisfies the structural decreasing condition.

When the system accepts a fixpoint, it now prints which decreasing argument 
was used, e.g:

 plus is recursively defined (decreasing on 1st argument)

The search is quite brute-force, and may need to be optimized for huge mutual
fixpoints (?). Anyway, writing explicit {struct} is always a possible fallback.

N.B. in the standard library, only 4 functions have an decreasing argument 
different from the one that would be automatically infered: 
  List.nth, List.nth_ok, List.nth_error, FMapPositive.xfind
And compiling with as few explicit struct as possible would add about 15s 
in compilation time for the whole standard library. 




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

0 files changed, 0 insertions, 0 deletions