diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-05-16 19:46:52 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-05-16 19:46:52 +0200 |
| commit | aca979230e6ff72913c63b844954f1ec9dc24d61 (patch) | |
| tree | 096b69c8a74816a59948480b5536004e4588f263 /doc | |
| parent | 8f7bfd85b92c00e1d0c88a07f4a0e6febcfadaf0 (diff) | |
| parent | 35eedc8e0878a174af2688913b6b60c879cf435c (diff) | |
Merge PR #7535: Typo in documentation of Derive
Diffstat (limited to 'doc')
| -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 |