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`.
---
 tools/gallina-syntax.el | 4 +---
 tools/gallina_lexer.mll | 1 -
 2 files changed, 1 insertion(+), 4 deletions(-)

(limited to 'tools')

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 }
-- 
cgit v1.2.3