From 47e5f716f7ded0eec43b00d49955d56c370c3596 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 8 Jun 2008 16:13:37 +0000
Subject: - 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
---
 doc/common/macros.tex | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'doc/common')

diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index 6b6c158b51..1c4fa7e1f9 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}}
-- 
cgit v1.2.3