Convert rewriting and proof-mode chapters to prodn

2 files changed, 7 insertions, 7 deletions

diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index d20a82e6c0..7ad2605f4a 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -43,7 +43,7 @@ Batch compilation (coqc)
 ------------------------
 
 The ``coqc`` command takes a name *file* as argument. Then it looks for a
-vernacular file named *file*.v, and tries to compile it into a
+file named *file*.v, and tries to compile it into a
 *file*.vo file (See :ref:`compiled-files`).
 
 .. caution::
@@ -434,7 +434,7 @@ wrong. In the current version, it does not modify the compiled libraries to mark
 them as successfully checked.
 
 Note that non-logical information is not checked. By logical
-information, we mean the type and optional body associated to names.
+information, we mean the type and optional body associated with names.
 It excludes for instance anything related to the concrete syntax of
 objects (customized syntax rules, association between short and long
 names), implicit arguments, etc.
diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst
index c239797cc2..dcc60195ed 100644
--- a/doc/sphinx/practical-tools/coqide.rst
+++ b/doc/sphinx/practical-tools/coqide.rst
@@ -7,7 +7,7 @@ Coq Integrated Development Environment
 
 The Coq Integrated Development Environment is a graphical tool, to be
 used as a user-friendly replacement to `coqtop`. Its main purpose is to
-allow the user to navigate forward and backward into a Coq vernacular
+allow the user to navigate forward and backward into a Coq
 file, executing corresponding commands or undoing them respectively.
 
 CoqIDE is run by typing the command `coqide` on the command line.
@@ -100,10 +100,10 @@ processed color, though their preceding proofs have the processed color.
 Notice that for all these buttons, except for the "gears" button, their operations
 are also available in the menu, where their keyboard shortcuts are given.
 
-Vernacular commands, templates
------------------------------------
+Commands and templates
+----------------------
 
-The Templates menu allows using shortcuts to insert vernacular
+The Templates menu allows using shortcuts to insert
 commands. This is a nice way to proceed if you are not sure of the
 syntax of the command you want.
 
@@ -116,7 +116,7 @@ Queries
 .. image:: ../_static/coqide-queries.png
    :alt: CoqIDE queries
 
-We call *query* any vernacular command that does not change the current state,
+We call *query* any command that does not change the current state,
 such as ``Check``, ``Search``, etc. To run such commands interactively, without
 writing them in scripts, CoqIDE offers a *query pane*. The query pane can be
 displayed on demand by using the ``View`` menu, or using the shortcut ``F1``.