| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2021-04-21 | Document the "Proof using" requirement for 'proof-omit-proofs-option | Erik Martin-Dorel | |
| 2021-04-16 | document the omit proofs feature manual and changes file | Hendrik Tews | |
| 2021-03-21 | Fix #563 avoid dual-send bug in search blacklist customization. | Pierre Courtieu | |
| 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. | |||
| 2021-02-25 | docs(CHANGES): Add "M-x proof-upgrade-elpa-packages RET" & menu item | Erik Martin-Dorel | |
| 2021-02-13 | update changes and documentation for vok feature | Hendrik Tews | |
| 2020-09-11 | fix(CHANGES): spelling of "whether" (#511) | dymil | |
| 2020-04-15 | add CHANGES entry for vos | Hendrik Tews | |
| 2020-04-15 | Span menu entry for proof using annotation + doc. | Pierre Courtieu | |
| 2020-04-10 | docs: Update CHANGES after issue #479 and PR #480 | Erik Martin-Dorel | |
| * Make (coq-insert-intros) conditionnaly insert `move=>` or `intros` | |||
| 2020-04-09 | Automatic "Proof using" insertion. | Pierre Courtieu | |
| When "Suggest Proof Using" is set in coq, coq suggests "Proof using" annotations. We insert these annotation (by default after asking the user). | |||
| 2020-01-19 | Generic monadic indentation + specifically ext-lib / Compcert + doc. | Pierre Courtieu | |
| This a generalization of PR#451 proposed by @Chobbes. Since these syntax are not completely universal (and not builtin in coq), the idea is to make the syntax customizable, especially to make it possible to disable it. NOTE: to make the Compcert syntax supported I had to refine the smie lexer so that the ";" token was emitted as a fllback instead of "; tactic". NOTE2: I had to make the coq-user-token and coq-monadic-tokens be tested ON THE RESULT of smie-coq-backward-token. | |||
| 2019-05-16 | Highlight diffs in goals and some error messages | Jim Fehrle | |
| using Coq's proof diffs feature. | |||
| 2018-08-22 | Bump version from 4.4.1~pre to 4.5-git | Erik Martin-Dorel | |
| This commit ensures the version number is (version-to-list)-compliant. | |||
| 2018-06-11 | key maps + small glitch hyp highlight/folding code. | Pierre Courtieu | |
| 2018-06-08 | Changed the look of folding/unfolding hyps. | Pierre Courtieu | |
| 2018-06-04 | Shorter CHANGES + smal fixes in hide/highlight hyps code. | Pierre Courtieu | |
| 2018-06-01 | Click hypothesis to (un)hide them. | Pierre Courtieu | |
| 2018-05-31 | Updated CHANGES about hiding and highlighting of hyps. | Pierre Courtieu | |
| 2018-02-20 | Bind C-c C-m (= C-c RET) to proof-goto-point [tty] (#228) | Erik Martin-Dorel | |
| Close ProofGeneral/PG#31 | |||
| 2017-11-06 | Prettier cheat face (background + box). | Pierre Courtieu | |
| 2017-10-26 | Updating CHANGES with lexer extensibility. | Pierre Courtieu | |
| 2017-03-03 | Remove default key-binding for proof-electric-terminator-toggle. | Erik Martin-Dorel | |
| Close ProofGeneral/PG#160 | |||
| 2016-12-08 | documentation and CHANGES for coq-compile-keep-going | Hendrik Tews | |
| 2016-11-30 | write CHANGES | Hendrik Tews | |
| 2016-10-16 | Update CHANGES. | Erik Martin-Dorel | |
| Related: ProofGeneral/PG#41 | |||
| 2016-09-18 | Detail. | Erik Martin-Dorel | |
| 2016-09-18 | Promote CHANGES since 2820cb68 as related to PG 4.4. | Erik Martin-Dorel | |
| 2016-07-22 | Adding the option to highlight susual symbols. | Pierre Courtieu | |
| This may look ugly to the majority, so I let it off by default. I find it helpfull to have structuring symbols bold. | |||
| 2016-06-23 | Updating CHANGES. | Pierre Courtieu | |
| 2016-03-21 | updating CHANGES to the last commit. | Pierre Courtieu | |
| 2016-01-19 | Cleaning CHANGES. | Pierre Courtieu | |
| 2016-01-06 | updating CHANGES | Pierre Courtieu | |
| 2015-11-30 | Updated the CHANGES files, mainly git url. | Pierre Courtieu | |
| 2015-10-12 | proof-assert-command-hook added + Auto adjust width in coq mode. | Pierre Courtieu | |
| 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). | |||
| 2015-06-23 | Update to CHANGE. | Pierre Courtieu | |
| 2015-03-26 | A command to set coq printing width smartly. | Pierre Courtieu | |
| Set the width to the current goals window. Default binding: C-c C-a C-w. | |||
| 2015-03-13 | Added a command to send Queries to coq, with completion (C-c C-a C-q). | Pierre Courtieu | |
| 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. | |||
| 2015-03-09 | Added bug fixes in CHANGES. | Pierre Courtieu | |
| 2015-03-05 | Fixed stuff in CHANGES. | Pierre Courtieu | |
| 2015-03-05 | Customization variables for modules, section and proof indentation. | Pierre Courtieu | |
| 2015-03-04 | Fixed compilation issue with previous commit + CHANGE updates. | Pierre Courtieu | |
| 2015-02-03 | coloring names in resposne and goals | Pierre Courtieu | |
| 2015-01-27 | Fixed a bug in script navigation. Updated CHANGE | Pierre Courtieu | |
| 2015-01-14 | changed default indentation of match's cases. | Pierre Courtieu | |
| 2015-01-09 | Removing non-smie indentation + fix CHANGES. | Pierre Courtieu | |
| 2015-01-05 | trying to indent pending forall in the expected way | Pierre Courtieu | |
| 2014-12-23 | Supporting more bullets (coq 8.5), like ++ or ++++. | Pierre Courtieu | |
| 2014-06-04 | * coq-smie.el (coq-smie-.-deambiguate): Proofs don't start with a definition. | Stefan Monnier | |
| (coq-smie-backward-token): Don't burp at EOB. (coq-smie-rules): Indent top-level ":" like ":=". | |||
| 2013-07-04 | Fixing undeclared variables for compilation. | Pierre Courtieu | |
| 2013-06-21 | Added an entry to CHANGEs about coq project fields. | Pierre Courtieu | |
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |