diff options
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coq_commands.ml | 3 | ||||
| -rw-r--r-- | ide/coqide.ml | 4 |
2 files changed, 3 insertions, 4 deletions
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"); |