Opened 16 years ago

Closed 16 years ago

#172 closed defect (fixed)

Problem with indentation in Coq mode

Reported by: Alexandre Pilkiewicz Owned by: David Aspinall
Priority: minor Milestone: PG-Emacs-3.7
Component: 2:pg-emacs Keywords: indent script-indent
Cc:

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)

Change History (1)

comment:1 Changed 16 years ago by Proof General Developer

Resolution: → fixed
Status: new → closed

Now fixed. Many thanks for the report!

Code in coq-indent.el used proof-ass macro without doing (require 'proof-utils) so compiled incorrectly. Now have hard coded coq-script-indent instead. Also removed redefinition of proof-indent-line, and rearranged so a different setting can be used in derived mode (now: coq-indent-line).

Note: See TracTickets for help on using tickets.