diff options
| author | barras | 2003-11-13 18:02:09 +0000 |
|---|---|---|
| committer | barras | 2003-11-13 18:02:09 +0000 |
| commit | 9aab7ae10aa1d535734f336c4bce16d908576d65 (patch) | |
| tree | 34c92bbeaae2cc973dfbec48d921eae6934d9cdc /doc | |
| parent | 4c18a78b54ff33361990a6f19bcad69bb7a4417c (diff) | |
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
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/syntax-v8.tex | 6 |
1 files changed, 3 insertions, 3 deletions
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} |