| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
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
|
|
|
|
|
|
|
|
See INSTRUCTIONS and LIMITATIONS files for more details.
Currently works for flattening "packaged-up" tactic proofs into g/e commands.
Won't work for most proofs because most tactics/thms haven't been promoted.
Support for exporting proof graph as a series of goal pairs.
Support for displaying extra information to be intercepter by PG for Prooftree.
|
|
|
|
|
