diff options
Diffstat (limited to 'doc/sphinx/addendum/miscellaneous-extensions.rst')
| -rw-r--r-- | doc/sphinx/addendum/miscellaneous-extensions.rst | 16 |
1 files changed, 4 insertions, 12 deletions
diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst index b0343a8f0..b6c35d8fa 100644 --- a/doc/sphinx/addendum/miscellaneous-extensions.rst +++ b/doc/sphinx/addendum/miscellaneous-extensions.rst @@ -3,23 +3,15 @@ .. _miscellaneousextensions: Miscellaneous extensions -======================= - -:Source: https://coq.inria.fr/distrib/current/refman/miscellaneous.html -:Converted by: Paul Steckler - -.. contents:: - :local: - :depth: 1 ----- +======================== Program derivation ------------------ +------------------ |Coq| comes with an extension called ``Derive``, which supports program derivation. Typically in the style of Bird and Meertens or derivations of program refinements. To use the Derive extension it must first be -required with ``Require Coq.Derive.Derive``. When the extension is loaded, +required with ``Require Coq.derive.Derive``. When the extension is loaded, it provides the following command: .. cmd:: Derive @ident SuchThat @term As @ident @@ -28,7 +20,7 @@ The first `ident` can appear in `term`. This command opens a new proof presenting the user with a goal for term in which the name `ident` is bound to an existential variable `?x` (formally, there are other goals standing for the existential variables but they are shelved, as -described in Section :ref:`TODO-8.17.4`). +described in :tacn:`shelve`). When the proof ends two constants are defined: |