From 9aab7ae10aa1d535734f336c4bce16d908576d65 Mon Sep 17 00:00:00 2001
From: barras
Date: Thu, 13 Nov 2003 18:02:09 +0000
Subject: moins unaire au niveau 35, tactiques simple_induction et
 simple_destruct, Local devient Let

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4897 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/syntax-v8.tex | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'doc')

diff --git a/doc/syntax-v8.tex b/doc/syntax-v8.tex
index 429d0ab8ac..f22ad35165 100644
--- a/doc/syntax-v8.tex
+++ b/doc/syntax-v8.tex
@@ -420,11 +420,11 @@ $$
 \nlsep \TERM{specialize}~\OPT{\NT{int}}~\NT{constr-with-bindings}
 \nlsep \TERM{lapply}~\tacconstr
 %%
-\nlsep \TERM{simple_induction}~\NT{quantified-hyp}
+\nlsep \TERM{simple}~\TERM{induction}~\NT{quantified-hyp}
 \nlsep \TERM{induction}~\NT{induction-arg}~\OPT{\NT{with-names}}
        ~\OPT{\NT{eliminator}}
 \nlsep \TERM{double}~\TERM{induction}~\NT{quantified-hyp}~\NT{quantified-hyp}
-\nlsep \TERM{simple_destruct}~\NT{quantified-hyp}
+\nlsep \TERM{simple}~\TERM{destruct}~\NT{quantified-hyp}
 \nlsep \TERM{destruct}~\NT{induction-arg}~\OPT{\NT{with-names}}
        ~\OPT{\NT{eliminator}}
 \nlsep \TERM{decompose}~\TERM{record}~\tacconstr
@@ -816,7 +816,7 @@ $$
    \TERM{Theorem} ~\mid~ \TERM{Lemma} ~\mid~ \TERM{Fact} ~\mid~ \TERM{Remark}
 \SEPDEF
 \DEFNT{def-token}
-   \TERM{Definition} ~\mid~ \TERM{Local} ~\mid~
+   \TERM{Definition} ~\mid~ \TERM{Let} ~\mid~
    \OPT{\TERM{Local}}~\TERM{SubClass}
 \SEPDEF
 \DEFNT{assum-token}
-- 
cgit v1.2.3