diff options
| author |  Joachim Breitner <mail@joachim-breitner.de> | 2018-05-16 12:02:19 -0400 |
|---|---|---|
| committer | Joachim Breitner <mail@joachim-breitner.de> | 2018-05-16 12:02:19 -0400 |
| commit | 35eedc8e0878a174af2688913b6b60c879cf435c (patch) | |
| tree | 602aaeb0196a34a762260df236362bf322298c65 /doc/sphinx/addendum | |
| parent | d74d72419f5e9b68fe8ec9e8c046faecacf9f2f4 (diff) | |
Typo in documentation of Derive
Diffstat (limited to 'doc/sphinx/addendum')
| -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 80ea8a116..b6c35d8fa 100644 --- a/doc/sphinx/addendum/miscellaneous-extensions.rst +++ b/doc/sphinx/addendum/miscellaneous-extensions.rst @@ -11,7 +11,7 @@ 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 |