Merge PR#642: Small cleanup on `close_proof` type.

19 files changed, 26 insertions, 55 deletions

diff --git a/CHANGES b/CHANGES
index b5f6ba9279..31d691be0e 100644
--- a/CHANGES
+++ b/CHANGES
@@ -28,6 +28,8 @@ Vernacular Commands
 - Goals context can be printed in a more compact way when "Set
   Printing Compact Contexts" is activated.
 
+- The deprecated `Save` vernacular and its form `Save Theorem id` to
+  close proofs have been removed from the syntax. Please use `Qed`.
 
 Standard Library
 
diff --git a/dev/v8-syntax/syntax-v8.tex b/dev/v8-syntax/syntax-v8.tex
index 64431ea161..fa2864cec9 100644
--- a/dev/v8-syntax/syntax-v8.tex
+++ b/dev/v8-syntax/syntax-v8.tex
@@ -1158,7 +1158,7 @@ $$
 \nlsep \TERM{Abort}~\NT{ident}
 \nlsep \TERM{Existential}~\NT{num}~\KWD{:=}~\NT{constr-body}
 \nlsep \TERM{Qed}
-\nlsep \TERM{Save}~\OPTGR{\NT{thm-token}~\NT{ident}}
+\nlsep \TERM{Save}~\NT{ident}}
 \nlsep \TERM{Defined}~\OPT{\NT{ident}}
 \nlsep \TERM{Suspend}
 \nlsep \TERM{Resume}~\OPT{\NT{ident}}
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index 8ba28b32f1..0760d716e3 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -90,25 +90,12 @@ 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
   (and the following ones) can only be used if the original goal has
   been opened using the {\tt Goal} command.
 
-\item {\tt Save Theorem {\ident}.} \\
- {\tt Save Lemma {\ident}.} \\
- {\tt Save Remark {\ident}.}\\
- {\tt Save Fact {\ident}.}
- {\tt Save Corollary {\ident}.}
- {\tt Save Proposition {\ident}.}
-
-  Are equivalent to {\tt Save {\ident}.} 
 \end{Variants}
 
 \subsection[\tt Admitted.]{\tt Admitted.\comindex{Admitted}\label{Admitted}}
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.
 
diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex
index 0d537256bb..30b6304c16 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 d55e7f9dd7..5912bec357 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 0b7567a5ae..663e28d36a 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/intf/vernacexpr.mli b/intf/vernacexpr.mli
index cb093d85d5..94fa37eb69 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -143,6 +143,7 @@ type search_restriction =
 
 type rec_flag       = bool (* true = Rec;           false = NoRec          *)
 type verbose_flag   = bool (* true = Verbose;       false = Silent         *)
+                           (*   list of idents for qed exporting           *)
 type opacity_flag   = Opaque of lident list option | Transparent
 type coercion_flag  = bool (* true = AddCoercion    false = NoCoercion     *)
 type instance_flag  = bool option
@@ -223,7 +224,8 @@ type syntax_modifier =
 
 type proof_end =
   | Admitted
-  | Proved of opacity_flag * (lident * theorem_kind option) option
+  (*                         name in `Save ident` when closing goal *)
+  | Proved of opacity_flag * lident option
 
 type scheme =
   | InductionScheme of bool * reference or_by_notation * sort_expr
diff --git a/man/gallina.1 b/man/gallina.1
index 8c607216ed..f8879c457b 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 68b8be6b87..2def222905 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -48,14 +48,11 @@ 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 ->
-	  VernacEndProof (Proved (Opaque None,Some (id,None)))
+	  VernacEndProof (Proved (Opaque None, Some id))
       | IDENT "Defined" -> VernacEndProof (Proved (Transparent,None))
       |	IDENT "Defined"; id=identref ->
-	  VernacEndProof (Proved (Transparent,Some (id,None)))
+	  VernacEndProof (Proved (Transparent,Some id))
       | IDENT "Restart" -> VernacRestart
       | IDENT "Undo" -> VernacUndo 1
       | IDENT "Undo"; n = natural -> VernacUndo n
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 3e41439c8c..76f1d8dd71 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -721,9 +721,7 @@ open Decl_kinds
               | Opaque (Some l) ->
                   keyword "Qed" ++ spc() ++ str"export" ++
                     prlist_with_sep (fun () -> str", ") pr_lident l)
-          | Some (id,th) -> (match th with
-              | None -> (if opac <> Transparent then keyword "Save" else keyword "Defined") ++ spc() ++ pr_lident id
-              | Some tok -> keyword "Save" ++ spc() ++ pr_thm_token tok ++ spc() ++ pr_lident id)
+          | Some id -> (if opac <> Transparent then keyword "Save" else keyword "Defined") ++ spc() ++ pr_lident id
       )
       | VernacExactProof c ->
         return (hov 2 (keyword "Proof" ++ pr_lconstrarg c))
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 99fab08486..01f883cde1 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -82,7 +82,7 @@ type proof_object = {
 type proof_ending =
   | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * proof_universes
   | Proved of Vernacexpr.opacity_flag *
-             (Vernacexpr.lident * Decl_kinds.theorem_kind option) option *
+              Vernacexpr.lident option *
               proof_object
 type proof_terminator = proof_ending -> unit
 type closed_proof = proof_object * proof_terminator
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 6bb6f5e2cb..e90fb5bc93 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -70,7 +70,7 @@ type proof_ending =
   | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry *
 		  proof_universes
   | Proved of Vernacexpr.opacity_flag *
-             (Vernacexpr.lident * Decl_kinds.theorem_kind option) option *
+              Vernacexpr.lident option *
               proof_object
 type proof_terminator
 type closed_proof = proof_object * proof_terminator
diff --git a/test-suite/bugs/closed/348.v b/test-suite/bugs/closed/348.v
index 28cc5cb1e6..48f0b55129 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 4fc8d7c97d..6b6e83779f 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 12ddbda84e..f5bb884d27 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 c25abece15..662762b08c 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 449efd57cd..432b18e645 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 }
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index b79795aebd..0088b70790 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -280,13 +280,6 @@ let save_anonymous ?export_seff proof save_ident =
   check_anonymity id save_ident;
   save ?export_seff save_ident const cstrs pl do_guard persistence hook
 
-let save_anonymous_with_strength ?export_seff proof kind save_ident =
-  let id,const,(cstrs,pl),do_guard,_,hook = proof in
-  check_anonymity id save_ident;
-  (* we consider that non opaque behaves as local for discharge *)
-  save ?export_seff save_ident const cstrs pl do_guard
-      (Global, const.const_entry_polymorphic, Proof kind) hook
-
 (* Admitted *)
 
 let warn_let_as_axiom =
@@ -337,9 +330,7 @@ let universe_proof_terminator compute_guard hook =
 	(hook (Some (fst proof.Proof_global.universes))) is_opaque in
       begin match idopt with
       | None -> save_named ~export_seff proof
-      | Some ((_,id),None) -> save_anonymous ~export_seff proof id
-      | Some ((_,id),Some kind) -> 
-          save_anonymous_with_strength ~export_seff proof kind id
+      | Some (_,id) -> save_anonymous ~export_seff proof id
       end;
       check_exist exports
   end