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

1 files changed, 11 insertions, 3 deletions

diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex
index 424e5047da..8ee30b8fb8 100644
--- a/doc/refman/RefMan-gal.tex
+++ b/doc/refman/RefMan-gal.tex
@@ -1329,9 +1329,8 @@ syntactical constraints on a special argument called the decreasing
 argument. They are needed to ensure that the {\tt Fixpoint} definition
 always terminates. The point of the {\tt \{struct \ident {\tt \}}}
 annotation is to let the user tell the system which argument decreases
-along the recursive calls. This annotation may be left implicit for
-fixpoints where only one argument has an inductive type. For instance,
-one can define the addition function as :
+along the recursive calls. For instance, one can define the addition 
+function as :
 
 \begin{coq_example}
 Fixpoint add (n m:nat) {struct n} : nat :=
@@ -1341,6 +1340,15 @@ Fixpoint add (n m:nat) {struct n} : nat :=
   end.
 \end{coq_example}
 
+The {\tt \{struct \ident {\tt \}}} annotation may be left implicit, in
+this case the system try successively arguments from left to right
+until it finds one that satisfies the decreasing condition. Note that
+some fixpoints may have several arguments that fit as decreasing
+arguments, and this choice influences the reduction of the
+fixpoint. Hence an explicit annotation must be used if the leftmost
+decreasing argument is not the desired one. Writing explicit
+annotations can also speed up type-checking of large mutual fixpoints.
+
 The {\tt match} operator matches a value (here \verb:n:) with the
 various constructors of its (inductive) type. The remaining arguments
 give the respective values to be returned, as functions of the