diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-12-05 09:56:49 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-05 09:56:49 +0100 |
commit | 2ae7674c6788742c021988ac02caabceec958957 (patch) | |
tree | 8f8c17a32a4a77ace1eac05760847c8c12d35670 /doc | |
parent | 14c041012bd375cae018f83d107c836fca3d1f01 (diff) | |
parent | 6cb9ab00a62b87587b00147d4abd82e684220b03 (diff) |
Merge PR #6220: Use OCaml criteria for infix ops in extraction, #6212
Diffstat (limited to 'doc')
-rw-r--r-- | doc/refman/Extraction.tex | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex index 83e866e9f..79060e606 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 => "(*)" [ "(,)" ]. |