diff options
Diffstat (limited to 'doc/refman')
| -rw-r--r-- | doc/refman/Extraction.tex | 8 | ||||
| -rw-r--r-- | doc/refman/RefMan-com.tex | 5 |
2 files changed, 8 insertions, 5 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-com.tex b/doc/refman/RefMan-com.tex index 8b1fc7c8f3..b4d9f60ebc 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -299,8 +299,9 @@ The following command-line options are recognized by the commands {\tt \section{Compiled libraries checker ({\tt coqchk})} -The {\tt coqchk} command takes a list of library paths as argument. -The corresponding compiled libraries (.vo files) are searched in the +The {\tt coqchk} command takes a list of library paths as argument, described +either by their logical name or by their physical filename, which must end in +{\tt .vo}. The corresponding compiled libraries (.vo files) are searched in the path, recursively processing the libraries they depend on. The content of all these libraries is then type-checked. The effect of {\tt coqchk} is only to return with normal exit code in case of success, |