Unification de TacLetRecIn et TacLetIn. En particulier, on peut

maintenant écrire des fonctions récursives qui n'ont pas l'apparence
d'être fonctionnelle. La sémantique reste toutefois différente. Par
exemple, dans

Ltac is := 
  let rec i := match goal with |- ?A -> ?B => intro; i | _ => idtac end in
  i.

l'évaluation de i est paresseuse, alors que dans une version non récursive

Ltac is := 
  let i := match goal with |- ?A -> ?B => intro | _ => idtac end in
  i.

l'évaluation de i est forte (et échoue sur le "match" qui n'est pas
autorisé à retourner une tactique).

(note: code mort dans tactics.ml en passant + indexation Implicit Type dans doc)


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

2 files changed, 7 insertions, 10 deletions

diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index da39b1d3d..00eb5c6d2 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1356,6 +1356,7 @@ Print Canonical Projections.
 \end{coq_example}
 
 \subsection{Implicit types of variables}
+\comindex{Implicit Types}
 
 It is possible to bind variable names to a given type (e.g. in a
 development using arithmetic, it may be convenient to bind the names
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index af9241e9d..d9a1d4756 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -18,7 +18,7 @@ problems.
 \def\tacexprinf{\textrm{\textsl{tacexpr$_2$}}}
 \def\tacexprpref{\textrm{\textsl{tacexpr$_3$}}}
 \def\atom{\textrm{\textsl{atom}}}
-\def\recclause{\textrm{\textsl{rec\_clause}}}
+%%\def\recclause{\textrm{\textsl{rec\_clause}}}
 \def\letclause{\textrm{\textsl{let\_clause}}}
 \def\matchrule{\textrm{\textsl{match\_rule}}}
 \def\contextrule{\textrm{\textsl{context\_rule}}}
@@ -109,12 +109,9 @@ is understood as
 {\tacexprlow} & ::= &
 {\tt fun} \nelist{\name}{} {\tt =>} {\atom}\\
 & | &
-{\tt let} \nelist{\letclause}{\tt with} {\tt in}
+{\tt let} \zeroone{\tt rec} \nelist{\letclause}{\tt with} {\tt in}
 {\atom}\\
 & | &
-{\tt let rec} \nelist{\recclause}{\tt with} {\tt in}
-{\tacexpr}\\
-& | &
 {\tt match goal with} \nelist{\contextrule}{\tt |} {\tt end}\\
 & | &
 {\tt match reverse goal with} \nelist{\contextrule}{\tt |} {\tt end}\\
@@ -168,8 +165,6 @@ is understood as
 \\
 \letclause & ::= & {\ident} \sequence{\name}{} {\tt :=} {\tacexpr}\\
 \\
-\recclause & ::= & {\ident} \nelist{\name}{} {\tt :=} {\tacexpr}\\
-\\
 \contextrule & ::= &
   \nelist{\contexthyps}{\tt ,} {\tt |-}{\cpattern} {\tt =>} {\tacexpr}\\
 & $|$ & {\tt |-} {\cpattern} {\tt =>} {\tacexpr}\\
@@ -215,7 +210,7 @@ which is then applied to the current goal.
 
 There is a special case for {\tt match goal} expressions of which
 the clauses evaluate to tactics. Such expressions can only be used as
-end result of a tactic expression (never as argument of a local
+end result of a tactic expression (never as argument of a non recursive local
 definition or of an application).
 
 The rest of this section explains the semantics of every construction
@@ -444,8 +439,9 @@ for $i=1,...,n$. There is no dependencies between the {\tacexpr}$_i$
 and the {\ident}$_i$.
 
 Local definitions can be recursive by using {\tt let rec} instead of
-{\tt let}. Only functions can be defined by recursion, so at least one
-argument is required.
+{\tt let}. In this latter case, the definitions are evaluated lazily
+so that the {\tt rec} keyword can be used also in non recursive cases
+so as to avoid the eager evaluation of local definitions.
 
 \subsubsection{Application}