Opened 14 years ago
Closed 14 years ago
#331 closed enhancement (fixed)
Coq config for proof-goal-command and proof-save-command
| Reported by: | Erik Martin-Dorel | Owned by: | David Aspinall |
|---|---|---|---|
| Priority: | minor | Milestone: | PG-Emacs-4.0 |
| Component: | 7:prover-coq | Keywords: | |
| Cc: | erik.martin-dorel@… |
Description
The convenient functions proof-issue-goal and proof-issue-save
rely on the variables proof-goal-command and proof-save-command
which are currently set to "Goal %s . " and "Save %s . " in coq/coq.el
I would suggest to remove the unnecessary last-but-one spaces: "Goal %s. " and "Save %s. " will be closer to Coq standard phrasing.
Kind regards, Erik.
Change History (2)
comment:1 Changed 14 years ago by
| Cc: | erik.martin-dorel@… added |
|---|
comment:2 Changed 14 years ago by
| Resolution: | → fixed |
|---|---|
| Status: | new → closed |
Note: See
TracTickets for help on using
tickets.
Done, thanks.