diff options
| author | Jim Fehrle | 2018-11-28 10:35:27 -0800 |
|---|---|---|
| committer | Jim Fehrle | 2018-12-04 13:16:26 -0800 |
| commit | 9903f6a7f86661549def884a0050d0f4537d52d7 (patch) | |
| tree | e18757b500abeeab710c99f506d79259ba18260e /doc/sphinx/addendum | |
| parent | 40c483a95f354e457e10d00951fd6a8eec08176d (diff) | |
Add undocumented options from mattam82
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/extraction.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 8 | ||||
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 5 |
3 files changed, 13 insertions, 4 deletions
diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index 8891234330..e93b01f14d 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -422,7 +422,7 @@ Additional settings :name: Extraction Flag Controls which optimizations are used during extraction, providing a finer-grained - control than :flag:`Extraction Optimize`. The bits of *num* are used as a bit mask. + control than :flag:`Extraction Optimize`. The bits of :token:`num` are used as a bit mask. Keeping an option off keeps the extracted ML more similar to the Coq term. Values are: @@ -454,7 +454,7 @@ Additional settings .. flag:: Extraction TypeExpand - If set, fully expand Coq types in ML. **see type_expand in mlutil.ml** + If set, fully expand Coq types in ML. See the Coq source code to learn more. Differences between |Coq| and ML type systems ---------------------------------------------- diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index 429dcbee69..56f84d0ff0 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -95,6 +95,14 @@ coercions. (the option is on by default). Coercion of subset types and pairs is still active in this case. +.. flag:: Program Mode + + Enables the program mode, in which 1) typechecking allows subset coercions and + 2) the elaboration of pattern matching of :cmd:`Program Fixpoint` and + :cmd:`Program Definition` act + like Program Fixpoint/Definition, generating obligations if there are + unresolved holes after typechecking. + .. _syntactic_control: Syntactic control over equalities diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 7933cdaee0..43d302114e 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -556,7 +556,8 @@ Settings Determines how much information is shown for typeclass resolution steps during search. 1 is the default level. 2 shows additional information such as tried tactics and shelving - of goals. Setting this option also sets :flag:`Typeclasses Debug`. + of goals. Setting this option to 1 or 2 turns on :flag:`Typeclasses Debug`; setting this + option to 0 turns that option off. .. flag:: Refine Instance Mode @@ -579,7 +580,7 @@ Typeclasses eauto `:=` resolution tactic. The semantics of the options are: + ``debug`` In debug mode, the trace of successfully applied tactics is - printed. This value also be set with :flag:`Typeclasses Debug`. + printed. This value can also be set with :flag:`Typeclasses Debug`. + ``dfs, bfs`` This sets the search strategy to depth-first search (the default) or breadth-first search. This value can also be set with |