Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Add coq-Print-Ltac to print an Ltac term | John Grosen | 2018-08-07 |
| | |||
* | small fix on hyp overlays. | Pierre Courtieu | 2018-06-13 |
| | |||
* | Fix multiple hyp overlays. | Pierre Courtieu | 2018-06-13 |
| | | | | | queries would trigger re-generarion of overlays. Now overlays are generated if there are no overlays already. | ||
* | Fix the fix #355. | Pierre Courtieu | 2018-06-13 |
| | | | | The fix was bad: no ore hyps were foldable/highlightable. | ||
* | Small bug unhighlighting. | Pierre Courtieu | 2018-06-11 |
| | | | | | Selecting the unhighlightied hyps showed a different region color. Setting the face to nil is better. | ||
* | key maps + small glitch hyp highlight/folding code. | Pierre Courtieu | 2018-06-11 |
| | |||
* | Changed the look of folding/unfolding hyps. | Pierre Courtieu | 2018-06-08 |
| | |||
* | Shorter CHANGES + smal fixes in hide/highlight hyps code. | Pierre Courtieu | 2018-06-04 |
| | |||
* | Click hypothesis to (un)hide them. | Pierre Courtieu | 2018-06-01 |
| | |||
* | Fixed a typo in previous commits. | Pierre Courtieu | 2018-06-01 |
| | |||
* | Infrastructure for hypothesis hiding. | Pierre Courtieu | 2018-05-31 |
| | |||
* | Fixing infrastructure for hypothesis highlighting. | Pierre Courtieu | 2018-05-31 |
| | |||
* | Infrastructure for transient hyps highlighting. | Pierre Courtieu | 2018-05-31 |
| | |||
* | Fix typos in custom variable descriptions. (#236) | Tej Chajed | 2018-03-03 |
| | |||
* | Update copyright messages and improve the header of elisp files. | Erik Martin-Dorel | 2018-02-21 |
| | |||
* | Fix #214. | Pierre Courtieu | 2017-12-11 |
| | | | | If this works we should probably change the generic function as well. | ||
* | Fixing a bug with Set/Unset commands due to recent commits. | Pierre Courtieu | 2017-06-08 |
| | | | | | The "Show" inserted now and then would hide the result of Set/Unset commands. | ||
* | Adding a Set Silent + Show when backtracking into a proof. | Pierre Courtieu | 2017-06-06 |
| | | | | | Checking whether the backtrack is inside a proof or not is a bit convoluted but seems ok. | ||
* | Remove mmm and ML4PG contribs and remove references to them in code and docs | Paul Steckler | 2017-05-24 |
| | |||
* | Fixing Set/Unset Printing broken by auto "Show". | Pierre Courtieu | 2017-05-16 |
| | | | | | | Current coq trunk has a bug with Show that I reported (there is a spurious Show executed) which makes C-u C-c C-a C-s fail for now. Should be fixed shortly. | ||
* | temporary fix of automatic intros. | Pierre Courtieu | 2017-05-12 |
| | |||
* | Change (eval-when (compile) ...) to (eval-when-compile ...) | Clément Pit--Claudel | 2017-05-05 |
| | | | | This fixes a bunch of compilation warnings | ||
* | Merge pull request #157 from ProofGeneral/elpa | Clément Pit-Claudel | 2017-05-05 |
|\ | | | | | [WIP] ELPA/MELPA support | ||
* | | Preparing new warning tags (no more special chars). | Pierre Courtieu | 2017-04-24 |
| | | |||
* | | Added support for future new options (trunk). | Pierre Courtieu | 2017-03-22 |
| | | |||
| * | Add a FIXME in coq.el | Clément Pit--Claudel | 2017-03-08 |
| | | |||
| * | Remove compile-time calls to proof-ready-for-assistant | Clément Pit--Claudel | 2017-03-08 |
| | | | | | | | | | | Compilation used to run in a separate Emacs process for each file, but that's not what happens when installing PG with package.el. | ||
| * | Remove unnecessary calls to 'eval-and-compile' | Clément Pit--Claudel | 2017-03-08 |
| | | |||
| * | Fix incorrect uses of defvar | Clément Pit--Claudel | 2017-03-08 |
|/ | | | | | | | It didn't really matter that these variables were defined and set to nil during compilation, since we ran compilation in a clean Emacs in --batch mode; it does matter now, however, since package.el compiles PG in the user's currently running Emacs instance. | ||
* | get threeb frames only when needed | Paul Steckler | 2017-03-06 |
| | |||
* | one more redundant call removed | Paul Steckler | 2017-03-06 |
| | |||
* | remove redundant calls, simplify code | Paul Steckler | 2017-03-06 |
| | |||
* | Refreshing goal when Set Printing xxx. (#162) | Pierre Courtieu | 2017-03-03 |
| | | | | | * Close ProofGeneral/PG#161. Issue a "Show" each time a (Uns|S)et Printing is detected (and a proof is open). | ||
* | Fixing #154. | Pierre Courtieu | 2017-02-23 |
| | |||
* | save settings not defined with defpacustom (fixes #142) | Hendrik Tews | 2017-01-19 |
| | | | | | | | - infrastructure for saving/resetting customizations not defined with defpacustom - improve Coq -> Auto Compilation menu - polish documentation and manual | ||
* | Fix prooftree for Coq 8.6 | Hendrik Tews | 2017-01-14 |
| | | | | | | | In Coq 8.6 evar status printing is off by default, causing prooftree to crash. This patch inserts invisible commands to switch evar status printing on and off. This is done via the urgent-action-hook. | ||
* | add second argument to looking-back, required in emacs25 | Hendrik Tews | 2016-12-31 |
| | |||
* | properly reset the vio2vo delay timer | Hendrik Tews | 2016-12-28 |
| | | | | | cancel-timer does of course not set the variable that holds the timer to nil | ||
* | add quote to fix commit e3cc66dc2e60683531d75c12256d059ccbc64576 | Hendrik Tews | 2016-12-15 |
| | |||
* | fix :get for coq-search-blacklist | Hendrik Tews | 2016-12-15 |
| | |||
* | Merge pull request #101 from tchajed/print-universes-option | hendriktews | 2016-12-15 |
|\ | | | | | Add Set Printing Universes to options menu | ||
* | | fix customize-group coq | Hendrik Tews | 2016-11-30 |
| | | |||
| * | Add Set Printing Universes to options menu | Tej Chajed | 2016-08-15 |
|/ | |||
* | Replace "Set Implicit Arguments" option with "Set Printing Implicit". | Erik Martin-Dorel | 2016-08-14 |
| | | | | Closes #99. | ||
* | Coq: option to prefer top over bottom of concl. | Pierre Courtieu | 2016-06-23 |
| | |||
* | Merge branch 'master' of github.com:ProofGeneral/PG | Pierre Courtieu | 2016-05-20 |
|\ | |||
* | | Fix #72+ make user keywords prioritized over default ones. | Pierre Courtieu | 2016-05-20 |
| | | |||
| * | Merge branch 'master' of github.com:ProofGeneral/PG | Clément Pit--Claudel | 2016-05-16 |
| |\ | |/ |/| | |||
| * | Don't offer "" as the default in C-c C-c C-a | Clément Pit--Claudel | 2016-05-16 |
| | | |||
* | | Merge branch 'master' of github.com:ProofGeneral/PG | Pierre Courtieu | 2016-05-02 |
|\| |