From 22b4d8c5b410e82f4bd1a78947d26e9dd4a3a6e3 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 22 May 2018 19:00:40 +0200
Subject: Workaround a weird error of .. coqtop::

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

diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index fff367fcd9..9438bf52d2 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -2691,7 +2691,7 @@ type classes inference.
   Full inference for ``ty``. The first subgoal demands a
   proof of such instantiated statement.
 
-+ .. coqtop:: in undo
++ .. coqdoc::
 
      have foo : ty := .
 
-- 
cgit v1.2.3