From 75715450906ffbf65a4f7a9f92031dd00ac96ead Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 24 Apr 2018 11:59:49 +0200
Subject: [sphinx] Fix a typo that appeared during the migration.

---
 doc/sphinx/practical-tools/coq-commands.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst
index 93dcfca4bf..83dddab4f5 100644
--- a/doc/sphinx/practical-tools/coq-commands.rst
+++ b/doc/sphinx/practical-tools/coq-commands.rst
@@ -171,7 +171,7 @@ and ``coqtop``, unless stated otherwise:
   Coq's auto-generated name scheme with names of the form *ident0*, *ident1*,
   etc. The command ``Set Mangle Names`` turns the behavior on in a document,
   and ``Set Mangle Names Prefix "ident"`` changes the used prefix. This feature
-  s intended to be used as a linter for developments that want to be robust to
+  is intended to be used as a linter for developments that want to be robust to
   changes in the auto-generated name scheme. The options are provided to
   facilitate tracking down problems.
 :-compat *version*: Attempt to maintain some backward-compatibility
-- 
cgit v1.2.3