From 35eedc8e0878a174af2688913b6b60c879cf435c Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 16 May 2018 12:02:19 -0400 Subject: Typo in documentation of Derive --- doc/sphinx/addendum/miscellaneous-extensions.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc') 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 -- cgit v1.2.3