Custom Query (361 matches)


Show under each result:

Results (10 - 12 of 361)

1 2 3 4 5 6 7 8 9 10 11 12 13 14
Ticket Resolution Summary Owner Reporter
#493 wontfix ProofGeneral stalls/loops on ... David Aspinall coquser

Goal True.


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

#492 fixed Proof General: script management confused, couldn't find goal span for save. when evaluating past the bottom of a module that contains a theorem with the same name as the module David Aspinall coquser

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.
    exact I.
End match_beta.

Module foo.
#491 wontfix Print Implicit not available as emacs command David Aspinall coquser

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.

1 2 3 4 5 6 7 8 9 10 11 12 13 14
Note: See TracQuery for help on using queries.