Opened 10 years ago
Closed 9 years ago
#491 closed defect (wontfix)
Print Implicit not available as emacs command
Reported by: | coquser | Owned by: | David Aspinall |
---|---|---|---|
Priority: | minor | Milestone: | PG-Emacs-4.3 |
Component: | 2:pg-emacs | Keywords: | |
Cc: |
Description
The command "Print Implicit <name>" is not made available as Emacs command by ProofGeneral, even though the "OTHER QUERIES" menu offers it. That command is really useful when dealing with lemmas that have implicit arguments, where printing the proof term is of no good use, but "Check" automatically instantiates (some of) the implicit arguments with global instances - so it's useless. (In fact, since I know about "Print Implicit", I don't see any reason at all to use Check.)
Steps to reproduce:
- In the "Coq" menu, select "OTHER QUERIES - Print Implicit..."
- Enter the name of some lemma or definition having implicit arguments
Actual behaviour:
- Emacs prints the name, term and type. It does *not* print any information concerning implicit arguments.
Expected behaviour:
- Emacs should do what "Print Implicit <name>" does: Print the name and type and implicit arguments, but not the term.
Further information:
- The menu entry "Print Implicit..." is mapped to the command coq-Print, which is the same command as "Print ...", so it's clear that the command does not behave as expected.
I am using version 4.3~pre130510 of ProofGeneral as packaged in Debian testing.
Change History (2)
comment:1 Changed 9 years ago by
comment:2 Changed 9 years ago by
Resolution: | → wontfix |
---|---|
Status: | new → closed |
Hi,
I won't apply this since it is redundant with About, which I consider better than Print Implicit. Do you see a reason to prefer the latter?
I agree that Check is less useful, except for real expressions (and not a simple constant). Maybe c-c c-a c-c should do About if given a simple id?
Here's a patch: