From 0dc203ee2983594fa064a84739d87f177636f18a Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 25 Apr 2018 21:14:59 +0200
Subject: Doc: Some quotes missing in file tactics.rst.

---
 doc/sphinx/proof-engine/tactics.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 3278bfd47c..064a540ec4 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -632,7 +632,7 @@ context. The new subgoal is :g:`U`.
 
 If the goal is a non-dependent product :g:`T`:math:`\rightarrow`:g:`U`, then it
 puts in the local context either :g:`Hn:T` (if :g:`T` is of type :g:`Set` or
-:g:`Prop`) or Xn:T (if the type of :g:`T` is :g:`Type`). The optional index
+:g:`Prop`) or :g:`Xn:T` (if the type of :g:`T` is :g:`Type`). The optional index
 ``n`` is such that ``Hn`` or ``Xn`` is a fresh identifier. In both cases, the
 new subgoal is :g:`U`.
 
-- 
cgit v1.2.3