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`.
---
 parsing/g_proofs.ml4 | 1 -
 1 file changed, 1 deletion(-)

(limited to 'parsing')

diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 68b8be6b87..53637439a8 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -48,7 +48,6 @@ GEXTEND Gram
       | IDENT "Qed" -> VernacEndProof (Proved (Opaque None,None))
       | IDENT "Qed"; IDENT "exporting"; l = LIST0 identref SEP "," ->
           VernacEndProof (Proved (Opaque (Some l),None))
-      | IDENT "Save" -> VernacEndProof (Proved (Opaque None,None))
       | IDENT "Save"; tok = thm_token; id = identref ->
 	  VernacEndProof (Proved (Opaque None,Some (id,Some tok)))
       | IDENT "Save"; id = identref ->
-- 
cgit v1.2.3