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 coquser

Here's a patch:

Index: coq/coq-abbrev.el
===================================================================
RCS file: /disk/cvs/proofgen/ProofGeneral/coq/coq-abbrev.el,v
retrieving revision 11.15
diff -u -r11.15 coq-abbrev.el
--- coq/coq-abbrev.el	26 Mar 2015 18:11:31 -0000	11.15
+++ coq/coq-abbrev.el	27 Apr 2015 15:02:24 -0000
@@ -165,7 +165,7 @@
      ["Print Section..." coq-PrintSection t]
      ""
      ["Locate notation..." coq-LocateNotation t]
-     ["Print Implicit..." coq-Print t]
+     ["Print Implicit..." coq-Print-implicit t]
      ["Print Scope/Visibility..." coq-PrintScope t])
     ("OPTIONS"
      ["Set Printing All" coq-set-printing-all t]

comment:2 Changed 9 years ago by courtieu

Resolution: wontfix
Status: newclosed

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?

Note: See TracTickets for help on using tickets.