- Extension de "generalize" en "generalize c as id at occs".

- Ajout clause "in" à "remember" (et passage du code en ML).
- Ajout clause "in" à "induction"/"destruct" qui, en ce cas, ajoute
  aussi une égalité pour se souvenir du terme sur lequel l'induction
  ou l'analyse de cas s'applique.
- Ajout "pose t as id" en standard (Matthieu: j'ai enlevé celui de
  Programs qui avait la sémantique de "pose proof" tandis que le nouveau
  a la même sémantique que "pose (id:=t)").
- Un peu de réorganisation, uniformisation de noms dans Arith, et
  ajout EqNat dans Arith.
- Documentation tactiques et notations de tactiques.



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

1 files changed, 3 insertions, 1 deletions

diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index 6b6c158b5..1c4fa7e1f 100755
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -125,7 +125,9 @@
 \newcommand{\caseitem}{\nterm{match\_item}}
 \newcommand{\eqn}{\nterm{equation}}
 \newcommand{\ifitem}{\nterm{dep\_ret\_type}}
-\newcommand{\letclauses}{\nterm{letclauses}}
+\newcommand{\convclause}{\nterm{conversion\_clause}}
+\newcommand{\occclause}{\nterm{occurrence\_clause}}
+\newcommand{\occset}{\nterm{occurrence\_set}}
 \newcommand{\params}{\nterm{params}} % vernac
 \newcommand{\returntype}{\nterm{return\_type}}
 \newcommand{\idparams}{\nterm{ident\_with\_params}}