From 92c604f8b331c3e202d8477019e183c2cfef9f41 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 29 Mar 2018 18:23:42 +0200
Subject: [Sphinx] Add chapter 29

Thanks to Clément Pit Claudel for porting this chapter.

Backport universe polymorphism changes from 2017 and 2018.
---
 doc/sphinx/proof-engine/proof-handling.rst | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

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

diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index 52cde52c69..adf3da3ebb 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -525,7 +525,9 @@ This variant displays a template of the Gallina
 
 .. exn:: Unknown inductive type
 
-.. exn:: Show Universes.
+.. _ShowUniverses:
+
+.. cmdv:: Show Universes.
 
 It displays the set of all universe constraints and
 its normalized form at the current stage of the proof, useful for
-- 
cgit v1.2.3