diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/addendum/extraction.rst | 13 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac2.rst | 7 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 29 |
3 files changed, 46 insertions, 3 deletions
diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index 7136cc28d1..d909f98956 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -313,14 +313,21 @@ The system also provides a mechanism to specify ML terms for inductive types and constructors. For instance, the user may want to use the ML native boolean type instead of the |Coq| one. The syntax is the following: -.. cmd:: Extract Inductive @qualid => @string [ {+ @string } ] +.. cmd:: Extract Inductive @qualid => @string__1 [ {+ @string } ] Give an ML extraction for the given inductive type. You must specify - extractions for the type itself (first :token:`string`) and all its - constructors (all the :token:`string` between square brackets). In this form, + extractions for the type itself (:n:`@string__1`) and all its + constructors (all the :n:`@string` between square brackets). In this form, the ML extraction must be an ML inductive datatype, and the native pattern matching of the language will be used. + When :n:`@string__1` matches the name of the type of characters or strings + (``char`` and ``string`` for OCaml, ``Prelude.Char`` and ``Prelude.String`` + for Haskell), extraction of literals is handled in a specialized way, so as + to generate literals in the target language. This feature requires the type + designated by :n:`@qualid` to be registered as the standard char or string type, + using the :cmd:`Register` command. + .. cmdv:: Extract Inductive @qualid => @string [ {+ @string } ] @string Same as before, with a final extra :token:`string` that indicates how to diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index dd80b29bda..b722b1af74 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -940,6 +940,13 @@ below will fail immediately and won't print anything. In any case, the value returned by the fully applied quotation is an unspecified dummy Ltac1 closure and should not be further used. +Switching between Ltac languages +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +We recommend using the :opt:`Default Proof Mode` option to switch between tactic +languages with a proof-based granularity. This allows to incrementally port +the proof scripts. + Transition from Ltac1 --------------------- diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 0527e26353..b1734b3f19 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -265,6 +265,35 @@ Name a set of section hypotheses for ``Proof using`` has remaining uninstantiated existential variables. It takes every uninstantiated existential variable and turns it into a goal. +Proof modes +``````````` + +When entering proof mode through commands such as :cmd:`Goal` and :cmd:`Proof`, +|Coq| picks by default the |Ltac| mode. Nonetheless, there exist other proof modes +shipped in the standard |Coq| installation, and furthermore some plugins define +their own proof modes. The default proof mode used when opening a proof can +be changed using the following option. + +.. opt:: Default Proof Mode @string + :name: Default Proof Mode + + Select the proof mode to use when starting a proof. Depending on the proof + mode, various syntactic constructs are allowed when writing an interactive + proof. The possible option values are listed below. + + - "Classic": this is the default. It activates the |Ltac| language to interact + with the proof, and also allows vernacular commands. + + - "Noedit": this proof mode only allows vernacular commands. No tactic + language is activated at all. This is the default when the prelude is not + loaded, e.g. through the `-noinit` option for `coqc`. + + - "Ltac2": this proof mode is made available when requiring the Ltac2 + library, and is set to be the default when it is imported. It allows + to use the Ltac2 language, as well as vernacular commands. + + - Some external plugins also define their own proof mode, which can be + activated via this command. Navigation in the proof tree -------------------------------- |