proof-general/CHANGES, branch master Emacs plugins for proof management systems Document the "Proof using" requirement for 'proof-omit-proofs-option 2021-04-20T22:29:10+00:00 Erik Martin-Dorel 2021-04-20T22:23:00+00:00 82311da10ee3dfa6f29ddfb9225f9f05c29dca31 






document the omit proofs feature manual and changes file
2021-04-16T20:53:05+00:00

Hendrik Tews

2021-03-21T14:55:38+00:00

c509eb17c1455972b967902a8ac34928717a8838












Fix #563 avoid dual-send bug in search blacklist customization.
2021-03-21T17:31:43+00:00

Pierre Courtieu

2021-03-19T12:34:00+00:00

0a0a34362ae4f7057f1cb1a0a12cf0a8ea3c0ce9

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.





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.







docs(CHANGES): Add "M-x proof-upgrade-elpa-packages RET" & menu item
2021-02-25T19:41:16+00:00

Erik Martin-Dorel

2021-02-25T19:36:44+00:00

1cddbe592b9e92b6e3c02358af7a1c7e1e301106












update changes and documentation for vok feature
2021-02-13T19:07:35+00:00

Hendrik Tews

2021-01-20T09:10:59+00:00

7e7af1294128bbccb98f6c44c77b7ab3ea863a42












fix(CHANGES): spelling of "whether" (#511)
2020-09-10T23:41:47+00:00

dymil

2020-09-10T23:41:47+00:00

8f609bd75a3388fcef78c76fb817ccb1cd63d82a












add CHANGES entry for vos
2020-04-15T16:05:31+00:00

Hendrik Tews

2020-04-12T09:30:58+00:00

8273e22e6da7b20e51fa330116bee20964d5dab8












Span menu entry for proof using annotation + doc.
2020-04-15T14:08:09+00:00

Pierre Courtieu

2020-04-10T20:48:55+00:00

97b8d4fcdcd67d49acd59389795fc48d9fa8f1d0












docs: Update CHANGES after issue #479 and PR #480
2020-04-10T21:13:26+00:00

Erik Martin-Dorel

2020-04-10T21:10:34+00:00

1ef1286c43d4d099b3b017069ed09c261eb8b6ca

* Make (coq-insert-intros) conditionnaly insert `move=>` or `intros`





* Make (coq-insert-intros) conditionnaly insert `move=>` or `intros`







Automatic "Proof using" insertion.
2020-04-09T13:20:09+00:00

Pierre Courtieu

2020-04-09T13:20:09+00:00

d3ac65007d676d57569d764b493d4d8d6f6ed1cb

When "Suggest Proof Using" is set in coq, coq suggests "Proof using"
annotations. We insert these annotation (by default after asking the
user).





When "Suggest Proof Using" is set in coq, coq suggests "Proof using"
annotations. We insert these annotation (by default after asking the
user).