From 2bc1ec34aa448278efb53342f17d62743ee245d2 Mon Sep 17 00:00:00 2001
From: Clément Pit-Claudel
Date: Wed, 25 Jul 2018 11:39:18 -0400
Subject: [sphinx] Do name cleanup in handle_signature

---
 doc/sphinx/proof-engine/detailed-tactic-examples.rst | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'doc/sphinx/proof-engine')

diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst
index 78719c1ef1..bb2a8741e2 100644
--- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst
+++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst
@@ -475,9 +475,8 @@ corresponding left-hand side and call yourself recursively on sub-
 terms. If there is no match, we are at a leaf: return the
 corresponding constructor (here ``f_const``) applied to the term.
 
-.. exn:: quote: not a simple fixpoint
-
-   Happens when ``quote`` is not able to perform inversion properly.
+When ``quote`` is not able to perform inversion properly, it will error out with
+:exn:`quote: not a simple fixpoint`.
 
 
 Introducing variables map
-- 
cgit v1.2.3