[vernac] Remove `Save.` command.

It has been deprecated for a while in favor of `Qed`.

12 files changed, 14 insertions, 26 deletions

diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 8ba28b32f..7e2b9db24 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 017de6d48..7e5bb81a9 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.
 
diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex
index 0d537256b..30b6304c1 100644
--- a/doc/tutorial/Tutorial.tex
+++ b/doc/tutorial/Tutorial.tex
@@ -385,13 +385,11 @@ apply H; [ assumption | apply H0; assumption ].
 
 Let us now save lemma \verb:distr_impl::
 \begin{coq_example}
-Save.
+Qed.
 \end{coq_example}
 
-Here \verb:Save: needs no argument, since we gave the name \verb:distr_impl: 
-in advance;
-it is however possible to override the given name by giving a different 
-argument to command \verb:Save:.
+Here \verb:Qed: needs no argument, since we gave the name \verb:distr_impl: 
+in advance.
 
 Actually, such an easy combination of tactics \verb:intro:, \verb:apply:
 and \verb:assumption: may be found completely automatically by an automatic
diff --git a/ide/coq_commands.ml b/ide/coq_commands.ml
index d55e7f9dd..5912bec35 100644
--- a/ide/coq_commands.ml
+++ b/ide/coq_commands.ml
@@ -105,8 +105,7 @@ let commands = [
    "Reset Extraction Inline";
    "Restore State";
    ];
-  [  "Save.";
-     "Scheme";
+  [  "Scheme";
      "Section";
      "Set Extraction AutoInline";
      "Set Extraction Optimize";
diff --git a/ide/coqide.ml b/ide/coqide.ml
index 0b7567a5a..663e28d36 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -1103,8 +1103,8 @@ let build_ui () =
 
   menu templates_menu [
     item "Templates" ~label:"Te_mplates";
-    template_item ("Lemma new_lemma : .\nProof.\n\nSave.\n", 6,9, "J");
-    template_item ("Theorem new_theorem : .\nProof.\n\nSave.\n", 8,11, "T");
+    template_item ("Lemma new_lemma : .\nProof.\n\nQed.\n", 6,9, "J");
+    template_item ("Theorem new_theorem : .\nProof.\n\nQed.\n", 8,11, "T");
     template_item ("Definition ident := .\n", 11,5, "E");
     template_item ("Inductive ident : :=\n  | : .\n", 10,5, "I");
     template_item ("Fixpoint ident (_ : _) {struct _} : _ :=\n.\n", 9,5, "F");
diff --git a/man/gallina.1 b/man/gallina.1
index 8c607216e..f8879c457 100644
--- a/man/gallina.1
+++ b/man/gallina.1
@@ -29,7 +29,7 @@ The suffix '.g' stands for Gallina.
 
 For that purpose, gallina removes all commands that follow a
 "Theorem", "Lemma", "Fact", "Remark" or "Goal" statement until it
-reaches a command "Abort.", "Save.", "Qed.", "Defined." or "Proof
+reaches a command "Abort.", "Qed.", "Defined." or "Proof
 <...>.". It also removes every "Hint", "Syntax",
 "Immediate"  or "Transparent" command.
 
@@ -52,7 +52,7 @@ Comments are removed in the *.g file.
 .SH NOTES
 
 Nested comments are correctly handled. In particular, every command
-"Save." or "Abort." in a comment is not taken into account.
+"Qed." or "Abort." in a comment is not taken into account.
 
 
 .SH BUGS
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 68b8be6b8..53637439a 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 ->
diff --git a/test-suite/bugs/closed/348.v b/test-suite/bugs/closed/348.v
index 28cc5cb1e..48f0b5512 100644
--- a/test-suite/bugs/closed/348.v
+++ b/test-suite/bugs/closed/348.v
@@ -9,5 +9,5 @@ End D.
 
 Module D' (M:S).
   Import M.
-  Definition empty:Set. exact nat. Save.
+  Definition empty:Set. exact nat. Qed.
 End D'.
diff --git a/test-suite/bugs/closed/38.v b/test-suite/bugs/closed/38.v
index 4fc8d7c97..6b6e83779 100644
--- a/test-suite/bugs/closed/38.v
+++ b/test-suite/bugs/closed/38.v
@@ -14,7 +14,7 @@ Definition same := fun (l m : liste) => forall (x : A), e x l <-> e x m.
 
 Definition same_refl (x:liste) : (same x x).
   unfold same; split; intros; trivial.
-Save.
+Qed.
 
 Goal forall (x:liste), (same x x).
   intro.
diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v
index 12ddbda84..f5bb884d2 100644
--- a/test-suite/success/dependentind.v
+++ b/test-suite/success/dependentind.v
@@ -15,7 +15,7 @@ Proof.
   intros n H.
   dependent destruction H.
   assumption.
-Save.
+Qed.
 
 Require Import ProofIrrelevance.
 
@@ -25,7 +25,7 @@ Proof.
   dependent destruction v.
   exists v ; exists a.
   reflexivity.
-Save.
+Qed.
 
 (* Extraction Unnamed_thm. *)
 
diff --git a/tools/gallina-syntax.el b/tools/gallina-syntax.el
index c25abece1..662762b08 100644
--- a/tools/gallina-syntax.el
+++ b/tools/gallina-syntax.el
@@ -390,7 +390,7 @@
     ("Corollary" "cor" "Corollary # : #.\nProof.\n#\nQed." t "Corollary")
     ("Declare Module :" "dmi" "Declare Module # : #.\n#\nEnd #." t)
     ("Declare Module <:" "dmi2" "Declare Module # <: #.\n#\nEnd #." t)
-    ("Definition goal" "defg" "Definition #:#.\n#\nSave." t);; careful
+    ("Definition goal" "defg" "Definition #:#.\n#\nQed." t);; careful
     ("Fact" "fct" "Fact # : #." t "Fact")
     ("Goal" nil "Goal #." t "Goal")
     ("Lemma" "l" "Lemma # : #.\nProof.\n#\nQed." t "Lemma")
@@ -492,7 +492,6 @@
      ("Require" nil "Require #." t "Require")
      ("Reserved Notation" nil "Reserved Notation" nil "Reserved\\s-+Notation")
      ("Reset Extraction Inline" nil "Reset Extraction Inline." t "Reset\\s-+Extraction\\s-+Inline")
-     ("Save" nil "Save." t "Save")
      ("Search" nil "Search #" nil "Search")
      ("SearchAbout" nil "SearchAbout #" nil "SearchAbout")
      ("SearchPattern" nil "SearchPattern #" nil "SearchPattern")
@@ -710,7 +709,6 @@ Used by `coq-goal-command-p'"
 
 (defvar coq-keywords-save-strict
   '("Defined"
-    "Save"
     "Qed"
     "End"
     "Admitted"
diff --git a/tools/gallina_lexer.mll b/tools/gallina_lexer.mll
index 449efd57c..432b18e64 100644
--- a/tools/gallina_lexer.mll
+++ b/tools/gallina_lexer.mll
@@ -105,7 +105,6 @@ and end_of_line = parse
   | _	  		{ print (Lexing.lexeme lexbuf) }
 
 and skip_proof = parse
-  | "Save."	{ end_of_line lexbuf }
   | "Save" space
                 { skip_until_point lexbuf }
   | "Qed."  	{ end_of_line lexbuf }