Custom Query (361 matches)

Goal nat -> nat -> nat.
intros ??.
       idatc.

Should not be indented this way. (Adding a space between the question marks does not fix things.)

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.

In my version of emacs + PG, Instance, Lemma, etc all get highlighted blue, but Proposition is the default text color.