diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-15 19:48:24 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-15 19:48:24 +0000 |
| commit | 3675bac6c38e0a26516e434be08bc100865b339b (patch) | |
| tree | 87f8eb1905c7b508dea60b1e216f79120e9e772d /doc | |
| parent | c881bc37b91a201f7555ee021ccb74adb360d131 (diff) | |
modif existentielle (exists | --> exists ,) + bug d'affichage des pt fixes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5099 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/syntax-v8.tex | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/doc/syntax-v8.tex b/doc/syntax-v8.tex index 931c2fbc5..354222a15 100644 --- a/doc/syntax-v8.tex +++ b/doc/syntax-v8.tex @@ -591,7 +591,7 @@ has the keyword to be associated to \KWD{let} or to tactic \TERM{simpl} ? &5 &\RNAME{Then-seq} %% \nlsep \TERM{try} ~\NT{tactic} &3R &\RNAME{Try} -\nlsep \TERM{do} ~\NT{tactic} +\nlsep \TERM{do} ~\NT{int-or-var} ~\NT{tactic} \nlsep \TERM{repeat} ~\NT{tactic} \nlsep \TERM{progress} ~\NT{tactic} \nlsep \TERM{info} ~\NT{tactic} @@ -810,6 +810,7 @@ $$ \nlsep \NT{record-tok}~\OPT{\TERM{$>$}}~\NT{ident}~\STAR{\NT{binder-let}} ~\KWD{:}~\NT{constr}~\KWD{:=} ~\OPT{\NT{ident}}~\KWD{\{}~\NT{field-list}~\KWD{\}} +\nlsep \TERM{Ltac}~\NT{ltac-def}~\STARGR{~\TERM{with}~\NT{ltac-def}} \end{rules} \begin{rules} @@ -841,6 +842,9 @@ $$ \DEFNT{reduce} \TERM{Eval}~\NT{red-expr}~\KWD{in} \SEPDEF +\DEFNT{ltac-def} + \NT{ident}~\STAR{\NT{name}}~\KWD{:=}~\NT{tactic} +\SEPDEF %% TODO: with not. \DEFNT{inductive-definition} \OPT{\NT{string}}~\NT{ident}~\STAR{\NT{binder-let}}~\KWD{:} @@ -1061,8 +1065,7 @@ $$ %% TODO: min/maj pas a jour \begin{rules} \EXTNT{command} - \TERM{Ltac}~\NT{ident}~\STAR{\NT{name}}~\KWD{:=}~\NT{tactic} -\nlsep \TERM{Debug}~\TERM{On} + \TERM{Debug}~\TERM{On} \nlsep \TERM{Debug}~\TERM{Off} %% TODO: vernac \nlsep \TERM{Add}~\TERM{setoid}~\tacconstr~\tacconstr~\tacconstr |