proof-general/hol-light, branch master Emacs plugins for proof management systems Use `cl-lib` instead of `cl` everywhere 2018-12-13T15:35:04+00:00 Stefan Monnier 2018-12-12T20:20:08+00:00 632a3d7f9ded16faaf58e1c0769bcd4f7c8193e3 Use lexical-binding in a few files where it was easy. Don't require `proof-compat` when it's not used. * coq/coq-db.el: Use lexical-binding. * coq/coq-system.el: Use lexical-binding. (coq--extract-prog-args): Use concatenated-args rather than recomputing it. * coq/coq.el: Require `span` to silence some warnings. * generic/pg-user.el: Use lexical-binding. (complete, add-completion, completion-min-length): Silence warnings. * generic/pg-xml.el: Use lexical-binding. (pg-xml-string-of): Prefer mapconcat to reduce+concat. * generic/proof-depends.el: Use lexical-binding. (proof-dep-split-deps): Use `push`. * generic/proof-shell.el: Require `span` to silence some warnings. (proof-shell-invisible-command): Don't use lexical-let just to build a wasteful η-redex! * lib/holes.el: Use lexical-binding. Remove redundant :group args. * lib/span.el: Use lexical-binding. (span-read-only-hook): Use user-error. (span-raise): Remove, unused. 
Use lexical-binding in a few files where it was easy.
Don't require `proof-compat` when it's not used.

* coq/coq-db.el: Use lexical-binding.

* coq/coq-system.el: Use lexical-binding.
(coq--extract-prog-args): Use concatenated-args rather than recomputing it.

* coq/coq.el: Require `span` to silence some warnings.

* generic/pg-user.el: Use lexical-binding.
(complete, add-completion, completion-min-length): Silence warnings.

* generic/pg-xml.el: Use lexical-binding.
(pg-xml-string-of): Prefer mapconcat to reduce+concat.

* generic/proof-depends.el: Use lexical-binding.
(proof-dep-split-deps): Use `push`.

* generic/proof-shell.el: Require `span` to silence some warnings.
(proof-shell-invisible-command): Don't use lexical-let just to build
a wasteful η-redex!

* lib/holes.el: Use lexical-binding.
Remove redundant :group args.

* lib/span.el: Use lexical-binding.
(span-read-only-hook): Use user-error.
(span-raise): Remove, unused.
Cleanup patch; Moving defvar to toplevel 2018-12-12T17:28:39+00:00 Stefan Monnier 2018-12-11T23:48:51+00:00 a921439a4eb5b0d96182748e779c78e2f6a41a5f Move `defvar`s used to silence warnings outside of eval-when-compile. Make sure they don't actually give a value to the var. * pg-init.el: Simplify. Use (if t ...) to avoid running `require` at compile-time. Don't add subdirs to load-path here since this code is never used. (pg-init--script-full-path, pg-init--pg-root): Inline their definition into their sole user. * generic/proof-utils.el (proof-resize-window-tofit): Inline definitions of window-leftmost-p and window-rightmost-p previously in proof-compat.el. * lib/proof-compat.el (proof-running-on-win32): Remove, not used. (mac-key-mode): Remove, there's no carbon-emacs-package-version in Emacs≥24.3. (pg-custom-undeclare-variable): Use dolist. (save-selected-frame): Remove, save-selected-window also saves&restores the selected frame at the same time. Update all users (which already used save-selected-window around it). (window-leftmost-p, window-rightmost-p, window-bottom-p) (find-coding-system): Remove, unused. * hol-light/hol-light.el (caml-font-lock-keywords): Don't try to defvar it to a dummy value and... (hol-light): ...check its existence before using it instead. * coq/coq.el (coq-may-use-prettify): Simplify initialization. 
Move `defvar`s used to silence warnings outside of eval-when-compile.
Make sure they don't actually give a value to the var.

* pg-init.el: Simplify.
Use (if t ...) to avoid running `require` at compile-time.
Don't add subdirs to load-path here since this code is never used.
(pg-init--script-full-path, pg-init--pg-root):
Inline their definition into their sole user.

* generic/proof-utils.el (proof-resize-window-tofit):
Inline definitions of window-leftmost-p and window-rightmost-p previously
in proof-compat.el.

* lib/proof-compat.el (proof-running-on-win32): Remove, not used.
(mac-key-mode): Remove, there's no carbon-emacs-package-version in
Emacs≥24.3.
(pg-custom-undeclare-variable): Use dolist.
(save-selected-frame): Remove, save-selected-window also saves&restores
the selected frame at the same time.  Update all users (which already
used save-selected-window around it).
(window-leftmost-p, window-rightmost-p, window-bottom-p)
(find-coding-system): Remove, unused.

* hol-light/hol-light.el (caml-font-lock-keywords): Don't try to defvar
it to a dummy value and...
(hol-light): ...check its existence before using it instead.

* coq/coq.el (coq-may-use-prettify): Simplify initialization.
Update copyright messages and improve the header of elisp files. 2018-02-20T23:53:25+00:00 Erik Martin-Dorel 2017-08-12T11:48:08+00:00 4e0c2a00cfbb7ea5c5ab68573bfb0edb78e8bd6f 






Change (eval-when (compile) ...) to (eval-when-compile ...)
2017-05-05T16:10:58+00:00

Clément Pit--Claudel

2017-05-05T16:08:54+00:00

574b0992e3cb4b7a4ad88400b9a5ab0198a96ca5

This fixes a bunch of compilation warnings





This fixes a bunch of compilation warnings







Remove compile-time calls to proof-ready-for-assistant
2017-03-08T20:06:17+00:00

Clément Pit--Claudel

2017-02-26T00:35:35+00:00

98f2e463287e3562dc7b7126e062919a8604ca4a

Compilation used to run in a separate Emacs process for each file, but that's not
what happens when installing PG with package.el.





Compilation used to run in a separate Emacs process for each file, but that's not
what happens when installing PG with package.el.







Fix incorrect assumption that noninteractive == byte-compiling
2017-03-08T20:06:17+00:00

Clément Pit--Claudel

2017-02-26T05:28:18+00:00

70dfbc54d9a6b559dbfcfd6105a7e8c80d78d888

The PG Makefile does ensure (using --batch) that noninteractive is non-nil while
compiling, but package.el doesn't.





The PG Makefile does ensure (using --batch) that noninteractive is non-nil while
compiling, but package.el doesn't.







Improvements for type tokens, remove preceding colon
2015-01-05T11:41:31+00:00

David Aspinall

2015-01-05T11:41:31+00:00

855e97db6dc47848dc9c9193a35c4294b7ff7486












- support bullets and braces in Prooftree
2013-01-15T14:40:18+00:00

Hendrik Tews

2013-01-15T14:40:18+00:00

e1c67a6cb5ba78af5faf43b87c1869de5f3161b9

- prooftree protocol change to version 3





- prooftree protocol change to version 3







Update
2012-11-01T11:54:36+00:00

David Aspinall

2012-11-01T11:54:36+00:00

159ce79d0db889ea731d1b7d3202873205b1f1be












Remove option aspect of 'finfo' datatype, and rename datatype to 'mldata'.
2012-02-24T12:07:26+00:00

mark

2012-02-24T12:07:26+00:00

cf0c3e813e4601f7462268703efd5b14424bd6c3

Add wrapper function for :thm -> thm list.
Promote more objects.





Add wrapper function for :thm -> thm list.
Promote more objects.