From 0d7643dabade293696a377dbc1f858dff2d666f4 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Fri, 14 Sep 2018 13:35:47 +0200
Subject: Universe binders are Id, not Name. Never print Var.

Comes with minor cleanups in exception catching and unnecessary mapi.
---
 doc/sphinx/proof-engine/vernacular-commands.rst | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'doc')

diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 56df535d85..1e17a773a6 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -35,7 +35,7 @@ Displaying
    .. cmdv:: Print {? Term } @qualid\@@name
 
       This locally renames the polymorphic universes of :n:`@qualid`.
-      An underscore means the raw universe is printed.
+      An underscore means the usual name is printed.
 
 
 .. cmd:: About @qualid
@@ -49,7 +49,7 @@ Displaying
    .. cmdv:: About @qualid\@@name
 
       This locally renames the polymorphic universes of :n:`@qualid`.
-      An underscore means the raw universe is printed.
+      An underscore means the usual name is printed.
 
 
 .. cmd:: Print All
-- 
cgit v1.2.3