Opened 11 years ago

Closed 11 years ago

#475 closed defect (fixed)

[exists] tactic causes improper indentation

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

Description

Here is some code indented by TAB: 

Goal True.                                                                                                                                  
Proof.
  match goal with
    | _ => exists 1
                | _ => idtac
                  end.

Change History (1)

comment:1 Changed 11 years ago by courtieu

Resolution: → fixed
Status: new → closed

Thanks again for the report. Fixed.

Note: See TracTickets for help on using tickets.