From 2d31d956fb708add948d0126b7c616375abf6358 Mon Sep 17 00:00:00 2001
From: Joachim Breitner
Date: Mon, 1 Oct 2018 22:09:33 -0700
Subject: Docs: Missing backquote

---
 doc/sphinx/language/gallina-extensions.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst
index 636144e0c8..9dae7fd102 100644
--- a/doc/sphinx/language/gallina-extensions.rst
+++ b/doc/sphinx/language/gallina-extensions.rst
@@ -606,7 +606,7 @@ for several ways of defining a function *and other useful related
 objects*, namely: an induction principle that reflects the recursive
 structure of the function (see :tacn:`function induction`) and its fixpoint equality.
 The meaning of this declaration is to define a function ident,
-similarly to ``Fixpoint`. Like in ``Fixpoint``, the decreasing argument must
+similarly to ``Fixpoint``. Like in ``Fixpoint``, the decreasing argument must
 be given (unless the function is not recursive), but it might not
 necessarily be *structurally* decreasing. The point of the {} annotation
 is to name the decreasing argument *and* to describe which kind of
-- 
cgit v1.2.3