diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-07-13 23:40:33 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-07-13 23:40:33 +0200 |
| commit | f824657b2b0b42ff02d0c07337db1607e13f359f (patch) | |
| tree | 22f06b457451e88dcea25d190ec954021c800d77 /doc/sphinx/introduction.rst | |
| parent | ef62eddc084784fdc001e3e304a73a73568e7b8a (diff) | |
| parent | 6cdc4c69ea57f0498cc36f5213268920ca7f7d63 (diff) | |
Merge PR #8057: Fixed typos, wording and grammar errors in the Preamble of the Reference Manual (Introduction, Credits).
Diffstat (limited to 'doc/sphinx/introduction.rst')
| -rw-r--r-- | doc/sphinx/introduction.rst | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst index c7bc69db4..1a610396e 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -12,7 +12,7 @@ https://github.com/coq/coq/wiki#coq-tutorials). The |Coq| system is designed to develop mathematical proofs, and especially to write formal specifications, programs and to verify that -programs are correct with respect to their specification. It provides a +programs are correct with respect to their specifications. It provides a specification language named |Gallina|. Terms of |Gallina| can represent programs as well as properties of these programs and proofs of these properties. Using the so-called *Curry-Howard isomorphism*, programs, @@ -52,7 +52,7 @@ are processed from a file. How to read this book ===================== -This is a Reference Manual, so it is not made for a continuous reading. +This is a Reference Manual, so it is not intended for continuous reading. We recommend using the various indexes to quickly locate the documentation you are looking for. There is a global index, and a number of specific indexes for tactics, vernacular commands, and error messages and warnings. |