first check in of continuationals implementation

[helm.git] / helm / ocaml / tactics / doc / main.tex

diff --git a/helm/ocaml/tactics/doc/main.tex b/helm/ocaml/tactics/doc/main.tex
index be235a2c1fe9cdbecc73177a699034aee014b2f1..72639efb98805a9c7526f17f93f83efcc840cb35 100644 (file)
--- a/helm/ocaml/tactics/doc/main.tex
+++ b/helm/ocaml/tactics/doc/main.tex
@@ -21,7 +21,9 @@
 \newcommand{\APPLY}[1]{\ensuremath{\mathtt{apply}~\mathit{#1}}}
 \newcommand{\SKIP}{\ensuremath{\mathtt{skip}}}
 \newcommand{\TACTICAL}[1]{\ensuremath{\mathtt{tactical}~\mathit{#1}}}
-\newcommand{\SELECT}[2]{\ensuremath{\mathtt{select} ~ #1 ~ #2}}
+\newcommand{\OLDTACTICAL}[1]{\ensuremath{\mathtt{old\_tactical}~\mathit{#1}}}
+\newcommand{\SELECT}[1]{\ensuremath{\mathtt{select} ~ #1}}
+\newcommand{\ENDSELECT}[1]{\ensuremath{\mathtt{end}}}
 
 \newcommand{\GOAL}{\ensuremath{\mathit{goal}}}
 \newcommand{\GOALSWITCH}{\ensuremath{\mathit{goal\_switch}}}
@@ -54,18 +56,28 @@
 
 \[
 \begin{array}{rcll}
- C & ::= & & \mbox{(\textbf{continuationals})} \\
-   &     & C ~ \DOT & \mbox{(dot)} \\
-   &  |  & C ~ \SEMICOLON ~ C & \mbox{(semicolon)} \\
-   &  |  & \BRANCH & \mbox{(branch)} \\
-   &  |  & \SHIFT & \mbox{(shift)} \\
-   &  |  & \MERGE & \mbox{(merge)} \\
-   &  |  & \SELECT{n_1,\dots,n_k}{C} & \mbox{(select)} \\
-   &  |  & \TACTICAL{T} & \mbox{(tactical)} \\[2ex]
+ S & ::= & & \mbox{(\textbf{toplevel grammar})}\\
+   &     & \varepsilon & \\
+   &  |  & T~ P~ S & \\[2ex]
 
- T & ::= & & \mbox{(\textbf{tacticals})} \\
+ T & ::= & & \mbox{(\textbf{tactical})} \\
    &     & \APPLY{tac} & \mbox{(tactic application)} \\
    &  |  & \SKIP & \mbox{(closed goal skipping)} \\
+   &  |  & \OLDTACTICAL{tcl} & \mbox{(non step-by-step tactical)} \\
+   &  |  & \SELECT{n_1,\dots,n_k}{S} & \mbox{(select)} \\[2ex]
+
+ P & ::= & & \mbox{(\textbf{punctuation})} \\
+   &     & \DOT & \mbox{(dot)} \\
+   &  |  & \SEMICOLON & \mbox{(semicolon)} \\
+   &  |  & \BRANCH & \mbox{(branch)} \\
+   &  |  & \SHIFT & \mbox{(shift)} \\
+   &  |  & \MERGE ~ M & \mbox{(merge)} \\[2ex]
+
+ M & ::= & & \mbox{(\textbf{merge-punctuation})} \\
+   &     & \varepsilon & \\
+   &  |  & \MERGE ~ M& \mbox{(multi-merge)} \\
+   &  |  & \DOT & \mbox{(merge and choose)} \\[2ex]
+
 \end{array}
 \]