From 3c0d8d08bda81b9fbd7210e4e352a08bbe8219e8 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 17 May 2017 20:55:32 +0200
Subject: [vernac] Remove `Save.` command.

It has been deprecated for a while in favor of `Qed`.
---
 doc/refman/RefMan-pro.tex | 5 -----
 doc/refman/RefMan-tus.tex | 2 +-
 2 files changed, 1 insertion(+), 6 deletions(-)

(limited to 'doc/refman')

diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 8ba28b32f1..7e2b9db24d 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -90,11 +90,6 @@ memory overflow.
 
   Defines the proved term as a transparent constant.
 
-\item {\tt Save.}
-\comindex{Save}
-
-  This is a deprecated equivalent to {\tt Qed}.
-
 \item {\tt Save {\ident}.}
   
   Forces the name of the original goal to be {\ident}.  This command
diff --git a/doc/refman/RefMan-tus.tex b/doc/refman/RefMan-tus.tex
index 017de6d484..7e5bb81a90 100644
--- a/doc/refman/RefMan-tus.tex
+++ b/doc/refman/RefMan-tus.tex
@@ -707,7 +707,7 @@ Once all the existential variables have been defined the derivation is
 completed, and a construction can be generated from the proof tree,
 replacing each of the existential variables by its definition.  This
 is exactly what happens when one of the commands
-\texttt{Qed}, \texttt{Save} or \texttt{Defined} is invoked
+\texttt{Qed} or \texttt{Defined} is invoked
 (see Section~\ref{Qed}). The saved theorem becomes a defined constant,
 whose body is the proof object generated.
 
-- 
cgit v1.2.3