diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/Extraction.tex | 8 | ||||
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 9 |
2 files changed, 10 insertions, 7 deletions
diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex index 83e866e9f3..79060e6062 100644 --- a/doc/refman/Extraction.tex +++ b/doc/refman/Extraction.tex @@ -391,9 +391,11 @@ Extract Inductive bool => "bool" [ "true" "false" ]. Extract Inductive sumbool => "bool" [ "true" "false" ]. \end{coq_example} -\noindent If an inductive constructor or type has arity 2 and the corresponding -string is enclosed by parenthesis, then the rest of the string is used -as infix constructor or type. +\noindent When extracting to {\ocaml}, if an inductive constructor or type +has arity 2 and the corresponding string is enclosed by parentheses, +and the string meets {\ocaml}'s lexical criteria for an infix symbol, +then the rest of the string is used as infix constructor or type. + \begin{coq_example} Extract Inductive list => "list" [ "[]" "(::)" ]. Extract Inductive prod => "(*)" [ "(,)" ]. diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 5fb4585884..7034c56081 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -311,10 +311,11 @@ A sequence is an expression of the following form: \begin{quote} {\tacexpr}$_1$ {\tt ;} {\tacexpr}$_2$ \end{quote} -The expressions {\tacexpr}$_1$ and {\tacexpr}$_2$ are evaluated -to $v_1$ and $v_2$ which have to be tactic values. The tactic $v_1$ is -then applied and $v_2$ is applied to the goals generated by the -application of $v_1$. Sequence is left-associative. +The expression {\tacexpr}$_1$ is evaluated to $v_1$, which must be +a tactic value. The tactic $v_1$ is applied to the current goal, +possibly producing more goals. Then {\tacexpr}$_2$ is evaluated to +produce $v_2$, which must be a tactic value. The tactic $v_2$ is applied to +all the goals produced by the prior application. Sequence is associative. \subsubsection[Local application of tactics]{Local application of tactics\tacindex{[>\ldots$\mid$\ldots$\mid$\ldots]}\tacindex{;[\ldots$\mid$\ldots$\mid$\ldots]}\index{Tacticals![> \mid ]@{\tt {\tac$_0$};[{\tac$_1$}$\mid$\ldots$\mid$\tac$_n$]}}\index{Tacticals!; [ \mid ]@{\tt {\tac$_0$};[{\tac$_1$}$\mid$\ldots$\mid$\tac$_n$]}}} %\tacindex{; [ | ]} |