Custom Query – Proof General

Results (73 - 75 of 361)

← 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 →

Ticket	Resolution	Summary	Owner	Reporter
#170	fixed	Improve outline syntax for Isar	David Aspinall	David Aspinall
Description	Outline syntax only contains theory headings at the moment. Perhaps the indent-open category should be added?
#171	fixed	Documentation fix for Isabelle keybindings	David Aspinall	Mark A. Hillebrand
Description	Hi, the attached patch fixes the documentation of the special Isabelle (2007) key bindings in doc/ProofGeneral.texi with respect to isar/isar.el. The Proof General version against which the patch was made was ProofGeneral-3.7pre080117.
#172	fixed	Problem with indentation in Coq mode	David Aspinall	Alexandre Pilkiewicz
Description	While editing a Coq script proof file, the indentation does not work. In proof-General->Advanced-> Customize ->Proof user options, the Coq script ident option is activated. When I press tab, or M-x indent-according-to-mode, or M-x ident-region, I receive the message "Symbol's value as a variable is void: script-indent" Indentation works well in other mode like Tuareg I'm runing emacs 22.1.1 (i486-pc-linux-gnu, GTK+ Version 2.12.0) with ProofGeneral-3.7pre080117 and The Coq Proof Assistant, version 8.1pl3 (Dec. 2007)

← 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 →