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 +- doc/tutorial/Tutorial.tex | 8 +++----- ide/coq_commands.ml | 3 +-- ide/coqide.ml | 4 ++-- man/gallina.1 | 4 ++-- parsing/g_proofs.ml4 | 1 - test-suite/bugs/closed/348.v | 2 +- test-suite/bugs/closed/38.v | 2 +- test-suite/success/dependentind.v | 4 ++-- tools/gallina-syntax.el | 4 +--- tools/gallina_lexer.mll | 1 - 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 } -- cgit v1.2.3