diff options
| author | Maxime Dénès | 2017-05-24 02:37:26 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-05-24 02:37:26 +0200 |
| commit | 28f8da9489463b166391416de86420c15976522f (patch) | |
| tree | 5456aa680f6e54f7f7bf71f5c4d99dc4e8709e03 /tools | |
| parent | 05add9c71214bebf86f1892c5ad946cdce19009a (diff) | |
| parent | c1e9a27d383688e44ba34ada24fe08151cb5846e (diff) | |
Merge PR#642: Small cleanup on `close_proof` type.
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/gallina-syntax.el | 4 | ||||
| -rw-r--r-- | tools/gallina_lexer.mll | 1 |
2 files changed, 1 insertions, 4 deletions
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 } |