proof-general/coq, branch master Emacs plugins for proof management systems Merge pull request #559 from hendriktews/omit-proofs 2021-04-21T18:00:36+00:00 Erik Martin-Dorel 2021-04-21T18:00:36+00:00 b5c4c3a1423c7925194334d66c262054d6a6c4c5 Add feature to omit complete opaque proofs 
Add feature to omit complete opaque proofs
 add feature to omit complete opaque proofs 2021-04-16T20:53:05+00:00 Hendrik Tews 2021-03-14T22:07:37+00:00 e454ae013827b98b814c99ffbc1ca7f2525fb030 This commit adds a feature to recognize complete opaque proofs in the asserted region and to replace them with an admitted proof. This can drastically improve the processing time for the asserted region at the cost of not checking the omitted proofs. Omitted proofs are displayed slightly darker compared to other parts of the locked region. With this commit, the feature is supported for Coq for files in which proofs are started with some form of Proof and ended with either Qed, Defined, Admitted or Abort. To enable, configure proof-omit-proofs-option or click Proof General -> Quick Options -> Processing -> Omit Proofs. 
This commit adds a feature to recognize complete opaque proofs in
the asserted region and to replace them with an admitted proof.
This can drastically improve the processing time for the asserted
region at the cost of not checking the omitted proofs. Omitted
proofs are displayed slightly darker compared to other parts of
the locked region.

With this commit, the feature is supported for Coq for files in
which proofs are started with some form of Proof and ended with
either Qed, Defined, Admitted or Abort.

To enable, configure proof-omit-proofs-option or click
Proof General -> Quick Options -> Processing -> Omit Proofs.
Fixing "match with" generation. 2021-04-08T14:54:49+00:00 Pierre Courtieu 2021-04-08T14:54:49+00:00 d0acb626eba17023c55b002921870d60e48527a5 






Fix useless quotes generatinf warnings.
2021-04-08T14:50:47+00:00

Pierre Courtieu

2021-04-08T14:50:47+00:00

5dc5e6f085b1f2b2fb6a2ee6216b6d609310071b












Fixing hypothesis folding GUI.
2021-04-08T14:47:13+00:00

Pierre Courtieu

2021-04-08T09:46:40+00:00

9929d50bf33c3f72682713bbc2ef12ed21301407












Fix #562. Lazy/multi_?match indentation support.
2021-03-21T21:32:57+00:00

Pierre Courtieu

2021-03-21T18:25:49+00:00

f0f0476d07401aba2cf428a71f7ee960cd1b3154

Actually it seems that even multimatch and lazymatch was poorly
supported.





Actually it seems that even multimatch and lazymatch was poorly
supported.







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.







coq: Update coq-prettify-symbols-alist for consistency with company-coq
2021-03-17T04:36:48+00:00

Clément Pit-Claudel

2021-03-17T04:34:11+00:00

8ad13c2735c097238441244123214967be3894a0

There's no need for ("not" . ?¬) because Coq already has a "~" for it.





There's no need for ("not" . ?¬) because Coq already has a "~" for it.







protect uses of coq-callcoq
2021-02-22T22:25:30+00:00

Hendrik Tews

2021-02-22T22:00:41+00:00

76fe29c9b121a0010a0f24b5cca5ac706683e3c3

Uses of coq-callcoq need to correctly handle nil as result for
the case that coq-callcoq fails.

Additionally, add a regression test.

Fixes #551





Uses of coq-callcoq need to correctly handle nil as result for
the case that coq-callcoq fails.

Additionally, add a regression test.

Fixes #551







improve/fix code documentation for vok processing
2021-02-13T19:07:35+00:00

Hendrik Tews

2021-01-18T21:48:27+00:00

ecb3588482d4ec5b418eb566ecfd7e41d6addd6d