Opened 11 years ago

Closed 11 years ago

Last modified 11 years ago

#476 closed defect (fixed)

[Goal], [Proposition], [Intance], [Fixpoint], [Corollary] do not have indented proof scripts

Reported by: coquser Owned by: David Aspinall
Priority: minor Milestone: PG-Emacs-4.3
Component: 2:pg-emacs Keywords:
Cc: jasongross9+pg@…

Description

PG indents as follows 

Goal True.
constructor.
Qed.

Goal True.
Proof.
  constructor.
Qed.

And similarly for Proposition, Fixpoint, Instance, Corollary, and possibly some others. (Definition, Theorem, Lemma, and Let all work fine)

Change History (2)

comment:1 Changed 11 years ago by courtieu

Resolution: → fixed
Status: new → closed

Thanks! Fixed.

comment:2 Changed 11 years ago by courtieu

Coming back to this bug:

It is impossible to guess from the shape of an "Instance" command if it will generate goals or not. Therefore the only choice is to do *no* indentation and tell the user to put "Proof" to force indentation.

Note: See TracTickets for help on using tickets.