From 14787df2ea09994151e886bf918aca0aecbd8ade Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 24 Jan 2015 20:08:53 +0100
Subject: Reference Manual: Documenting new printing of evars and new effect of
 Set Printing Existential Instances (see bug report #3951).

---
 doc/refman/RefMan-pro.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'doc/refman/RefMan-pro.tex')

diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index eabb376395..df707ce941 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -239,7 +239,7 @@ proof was edited.
 
 This command instantiates an existential variable. {\tt \num}
 is an index in the list of uninstantiated existential variables
-displayed by {\tt Show Existentials.} (described in Section~\ref{Show})
+displayed by {\tt Show Existentials} (described in Section~\ref{Show}).
 
 This command is intended to be used to instantiate existential
 variables when the proof is completed but some uninstantiated
-- 
cgit v1.2.3