| Age | Commit message (Collapse) | Author |
|---|
|
Splitting the coq into two commands made me remove
coq-search-blacklist-string from defpgcustom. The visible effect is
that the menu entry has moved, and the command name changed. This is
explained in the CHANGES.
To squash.
|
|
New value vos-and-vok for coq-compile-vos customization option,
existing value vos stands now for vos-no-vok. The implementation
uses the existing vio2vo infrastructure with symbols vok and
vio2vo.
Documentation is still missing.
|
|
|
|
|
|
|
|
|
|
|
|
When "Suggest Proof Using" is set in coq, coq suggests "Proof using"
annotations. We insert these annotation (by default after asking the
user).
|
|
|
|
using Coq's proof diffs feature.
|
|
|
|
Fix a few more cl.el leftovers. Get rid of remaining use of iso-2022.
Use SMIE unconditionally.
* coq/coq-abbrev.el: Use lexical-binding.
(coq-install-abbrevs): Delete, only keep the relevant contents.
(proof-defstringset-fn): Remove. Fold changes into the main version.
* coq/coq-indent.el (coq-find-real-start): Use forward-comment.
* coq/coq-smie.el: Use lexical-binding. Assume `smie` is available.
(coq--string-suffix-p): Rename from coq-string-suffix-p.
Use string-suffix-p for it when available.
(string-suffix-p): Never define here. Change all users to use
coq--string-suffix-p instead.
(coq-smie-.-deambiguate): Use forward-comment. Remove unused var `beg`.
(coq-backward-token-fast-nogluing-dot-friends)
(coq-forward-token-fast-nogluing-dot-friends): Remove unused var
`tok-other`.
(coq-smie-search-token-backward): Remove unused var `p`.
(coq-smie-:=-deambiguate, coq-smie-backward-token): Prefer char-before
over looking-back.
(coq-smie-rules): Use `pcase` over deprecated cl's `case`.
* coq/coq-syntax.el: Use lexical-binding.
(coq-count-match): Rewrite so it doesn't do needless heap-allocation.
(coq-module-opening-p, coq-section-command-p, coq-goal-command-str-p):
Use case-fold-search rather than proof-string-match.
(coq-goal-command-regexp): Forward-declare.
(coq-save-command-regexp-strict): Move before first use.
(coq-reserved-regexp): Use a single \_< ... \_>.
(coq-detect-hyps-positions): Limit search for looking-back.
* coq/coq.el: Remove SMIE declarations since SMIE is always used.
(coq-use-smie): Remove, unused.
(coq-smie): Always require.
* generic/pg-pbrpm.el: Fix leftover cl.el uses.
* generic/proof-utils.el (proof-defstringset-fn): Fix copy&paste error
in the docstring, improve interactive prompt.
* lib/maths-menu.el: Use utf-8 and lexical-binding.
|
|
|
|
|
|
|
|
[WIP] ELPA/MELPA support
|
|
|
|
This file is `require'-d when compiling coq.el, and at that point the proof
assistant isn't set to coq yet, so it would define variables prefixed by `nil-'
instead of `coq'.
|
|
The PG Makefile does ensure (using --batch) that noninteractive is non-nil while
compiling, but package.el doesn't.
|
|
- infrastructure for saving/resetting customizations not defined
with defpacustom
- improve Coq -> Auto Compilation menu
- polish documentation and manual
|
|
Add Set Printing Universes to options menu
|
|
|
|
With this option set, compilation continues after the first error
to compile as much as possible and to potentially report more
than one error.
|
|
Making coq-compile-quick configurable via the Settings menu would
require a lot of work, because the
defpacustom/proof-menu-define-settings-menu engine does only work
for simple types. On second sight, I believe the Settings menu
and the whole engine behind it are more intended for options that
configure the proof assistant behind Proof General. Taking this
together, I believe, it makes more sense to have a separate menu
entry for auto compilation in the Coq menu. This submenu contains
all the options for background compilation. The compilation
entries from the settings menu should be deleted, probably after
the next release.
|
|
Select "Quick compilation mode" in the Coq menu. See also
documentation of coq-compile-quick, the and-vio2vo stuff is not yet
there.
|
|
|
|
|
|
Closes #99.
|
|
|
|
This hook was missing, it allows to send complete commands before
the (set of) command(s) sent by the user. It shall be used when
proof-shell-insert-hook cannot be used (because of multiple prompts
appearing).
|
|
Set the width to the current goals window.
Default binding: C-c C-a C-w.
|
|
Should replace C-c C-v at some point. Needs to have a complete list of
such queries. Obeys C-u prefix for Printing all flag.
|
|
|
|
|
|
|
|
menu, they are in option menu that only issues commands to the prover
and do not try to keep track of the values of the variables.
|
|
|
|
enabling it disables electric-terminator and vice-versa. In case both
are non nil at the same time, then electric teminator has priority. If
people like it we may propose this to other modes than coq.
+ fixed window layout policy.
|
|
'horizontal 'vertical 'smart policy.
|
|
|
|
|
|
Printing Implicit and Printing All flags.
|
|
* coq.el (coq-smie-grammar): Add rules for {|...|}, Let, Record, Module..End,
Section..End, and BeginSubproof..EndSubproof.
(coq-smie-search-token): New function.
(coq-smie-forward-token, coq-smie-backward-token): Recognize {| and |}.
Distinguish Module definition from Module introduction.
Merge "Module Type" and "Module".
(coq-smie-rules): Refine list-intro. Improve indentation after "with".
Add Function, Let and Record to the := case.
Indent within Module..End and friends. Improve indentation of record def.
Indent forall's body by 2. Better indent Lemmas.
* coq-db.el (coq-build-abbrev-table-from-db): Mark those abbrevs as `system'.
* coq-abbrev.el (coq-install-abbrevs): Don't bind save-abbrevs
since it's not needed any more.
|
|
|
|
|
|
buffer.
|
|
|
|
|
|
|
|
|
