search

snu-sf-class / pl2015spring

SNU 4190.310, 2015 Spring
11 stars 6 forks source link

Indentation problem in emacs with ProofGeneral #59

Closed minitu closed 9 years ago

minitu commented 9 years ago

I'm having a problem with indentation in emacs with ProofGeneral. It's supposed to insert 2 spaces or indent the same way as the above line when I press TAB but it often inserts a lot more spaces than that. I've searched for the solution online, and found that if I insert (require 'coq) in .emacs the indentation works properly but ProofGeneral does not execute. I wonder if anyone is experiencing the same problem and has found a solution to it.

jeehoonkang commented 9 years ago

It is a well-known problem that ProofGeneral sometimes cannot guess the precise size of spaces. I am not sure it is the case for you. To further investigate your case, I would like you to come to my office (mail pl2015@sf.snu.ac.kr for making appointment!).

Jeehoon