| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
versions of emacs.
|
|
|
|
|
|
coq-response buffer.
|
|
|
|
|
|
printing state as before.
|
|
coq-load-path) in the case of complex coq-load-path.
|
|
|
|
Printing Implicit and Printing All flags.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
version of smie indentation code was a good first try but this one is
much faster and cleaner. All desambiguations are done in the lexers,
it is still a bit slow on large proofs. Some bugs remain to be fixed.
|
|
|
|
|
|
given. Seems to work.
|
|
|
|
|
|
|
|
|
|
|
|
comment-start-skip: if it is already set then proof-script should not
change it. Ultimately if David approves we should moreover fix the
setting itself which is bugged.
coq-mode now sets this variable by itself.
|
|
|
|
set of rules. Fixed by cleaning rules.
|
|
+ bug fixes.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
- check if coq-load-path is well-formed
- update documentation
|
|
|
|
|
|
|
|
|
|
|
|
|
|
better fix.
|
|
+. is not accepted yet.
|
