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 /ide | |
| parent | 05add9c71214bebf86f1892c5ad946cdce19009a (diff) | |
| parent | c1e9a27d383688e44ba34ada24fe08151cb5846e (diff) | |
Merge PR#642: Small cleanup on `close_proof` type.
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 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"); |