diff options
Diffstat (limited to 'doc/sphinx/addendum/miscellaneous-extensions.rst')
| -rw-r--r-- | doc/sphinx/addendum/miscellaneous-extensions.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst index 3944a34cdc..7d30cae525 100644 --- a/doc/sphinx/addendum/miscellaneous-extensions.rst +++ b/doc/sphinx/addendum/miscellaneous-extensions.rst @@ -1,7 +1,7 @@ Program derivation ================== -|Coq| comes with an extension called ``Derive``, which supports program +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, |