| Commit message (Collapse) | Author | Age |
| |
|
|
|
|
|
|
| |
allows using a span attribute to detect goal commands.
I think I modified all modes accordingly.
|
|
|
|
|
| |
3rd 2004). I found another bug (infinite loop due to an error in
coq-back-to-indentation-prevline).
|
| |
|
| |
|
|
|
|
| |
does not use "proof-goal-command-p" and is not powerful enough.
|
|
|
|
|
|
|
|
|
| |
module start:
Module M:T with Definition A:=u.
I had to count the number of 'with' and ':=' to know if the last ':='
was a Module given explicitely (--> no module start) or only part of a
'with ...:=' (--> module start).
|
|
|
|
| |
not test the fsfemacs. Will do before release.
|
|
modification to better backtrack modules.
|