Opened 11 years ago

Closed 11 years ago

#478 closed defect (fixed)

[Proof <body term>.] messes up following indentation

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

Description

The following is some code indented with TAB:

Lemma foo : nat.                                                                                                                            
Proof 1.                                                                                                                                    
  Section Foo.                                                                                                                              
  End Foo.                                                                                                                                  
                                                                                                                                            
  Lemma bar : Type.                                                                                                                         
  Proof forall x, x.                                                                                                                        
    Check bar.

Change History (1)

comment:1 Changed 11 years ago by courtieu

Resolution: fixed
Status: newclosed

Thanks, should be fixed in cvs.

Proof. Proof with foo.

are goal starters, but

Proo foo.

is not.

Note: See TracTickets for help on using tickets.