| Age | Commit message (Collapse) | Author |
|---|
|
|
|
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
|
|
|
|
|
|
|
|
|
|
distributions with specific requirements (such as Debian with
debian-pkg-add-load-path-item) only need to patch one function.
|
|
|
|
without installing STIX.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Add wrapper function for :thm -> thm list.
Promote more objects.
|
|
|
|
|
|
|
|
|
|
Whole of examples3 now processes
Facility for adding manual labels to atomic/composite tactics
|
|
|
|
|
|
|
