Custom Query (361 matches)


Show under each result:

Results (7 - 9 of 361)

1 2 3 4 5 6 7 8 9 10 11 12 13
Ticket Resolution Summary Owner Reporter
#500 fixed Build fails, due to “'isar-markup-ml' is not known to be defined.” (PG 4.2, Mac OS 10.10.2, Aquamacs 3.2) David Aspinall coquser

I’m on Mac OS 10.10.2 (Yosemite), trying to build Proof General 4.2, for Aquamacs 3.2 (based on Emacs 24.4). Running make clean; make compile EMACS=/Applications/ fails with the error cascade

In toplevel form:
isar/isar-unicode-tokens.el:687:1:Error: the function `isar-markup-ml' is not known to be defined.
make[1]: *** [isar/isar-unicode-tokens.elc] Error 1
make: *** [compile] Error 2

Full make output at

#495 invalid Goals buffer aggressively cleared with Coq pre-8.5 David Aspinall coquser

I am using Proof General 4.3pre131011 with the current trunk version of Coq (pre-8.5).

With 8.4pl4, if I type period to end a tactic, my goals buffer update. If I delete the period, the goals buffer changes to what it had displayed immediately before. This is the desired behavior.

With 8.5pre, when I delete the period it clears the goals buffer, and does not display again until I press the period, making it extremely difficult to replay what changes a certain tactic made to my environment.

#494 fixed PG incorrectly parses the result of [Fail] in some cases David Aspinall coquser

In, e.g., the code

Ltac f := fail.
Goal True.
  Fail f.

coqtop -emacs returns

The command has indeed failed with message:
=> In nested Ltac calls to "f", last call failed.
Error: Tactic failure.

which PG assumes means that there was an error.

In other cases, PG sees "=> Error", which it takes to mean is not an error.

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