Custom Query (361 matches)

Goal True.

...

Evaluating this script (the "..." is literal) will cause PG to loop forever/stall while it waits for Coq to respond.

Here is a proof script that gives "Proof General: script management confused, couldn't find goal span for save." in PG 4.3pre131011 with Coq 8.4pl3 (December 2013):

Module match_beta.
  Theorem match_beta : True.
  Proof.
    exact I.
  Defined.
End match_beta.

Module foo.

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.