Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Fix most doc issues raised by (checkdoc) | 2018-08-23 | |
| | |||
* | Merge pull request #379 from tchajed/variant-keyword | 2018-08-21 | |
|\ | | | | | Support the Variant vernacular | ||
* \ | Merge branch 'master' of github.com:ProofGeneral/PG | 2018-08-18 | |
|\ \ | |||
* | | | Fix #7980, keep option order unchanged. | 2018-08-18 | |
| | | | |||
| | * | Support the Variant vernacular | 2018-08-17 | |
| |/ | | | | | | | | | Syntactically looks much like an Inductive, though it is non-recursive so "where" (mutual recursion) is not supported. | ||
| * | Add coq-Print-Ltac to print an Ltac term | 2018-08-07 | |
|/ | |||
* | Fixing last commit. | 2018-06-15 | |
| | |||
* | Fix #368 (emacs < 25 split-string has no trim arg). | 2018-06-15 | |
| | | | | Copied some code from company-coq. | ||
* | small fix on hyp overlays. | 2018-06-13 | |
| | |||
* | Fix multiple hyp overlays. | 2018-06-13 | |
| | | | | | queries would trigger re-generarion of overlays. Now overlays are generated if there are no overlays already. | ||
* | Fix the fix #355. | 2018-06-13 | |
| | | | | The fix was bad: no ore hyps were foldable/highlightable. | ||
* | Small bug unhighlighting. | 2018-06-11 | |
| | | | | | Selecting the unhighlightied hyps showed a different region color. Setting the face to nil is better. | ||
* | fix #355 + probable bug. | 2018-06-11 | |
| | | | | | By renaming the arg load-path into loadpath I notice that a coq-load-path was used instead of it. | ||
* | key maps + small glitch hyp highlight/folding code. | 2018-06-11 | |
| | |||
* | Changed the look of folding/unfolding hyps. | 2018-06-08 | |
| | |||
* | Small fix in a regexp. | 2018-06-06 | |
| | |||
* | Shorter CHANGES + smal fixes in hide/highlight hyps code. | 2018-06-04 | |
| | |||
* | Click hypothesis to (un)hide them. | 2018-06-01 | |
| | |||
* | Fixed a typo in previous commits. | 2018-06-01 | |
| | |||
* | Infrastructure for hypothesis hiding. | 2018-05-31 | |
| | |||
* | Fixing infrastructure for hypothesis highlighting. | 2018-05-31 | |
| | |||
* | Merge branch 'master' of github.com:ProofGeneral/PG | 2018-05-31 | |
|\ | |||
* | | Infrastructure for transient hyps highlighting. | 2018-05-31 | |
| | | |||
| * | small fix of face `coq-symbol-face' | 2018-04-22 | |
| | | |||
| * | Merge pull request #207 from SkySkimmer/master | 2018-04-08 | |
|/| | | | | | Make coq-prog-args safe when list of strings. | ||
* | | Fix typos in custom variable descriptions. (#236) | 2018-03-03 | |
| | | |||
* | | Update copyright messages and improve the header of elisp files. | 2018-02-21 | |
| | | |||
* | | typo in abbrevs. | 2018-02-07 | |
| | | |||
* | | look for vernac controls before focus bracket, fix for #223 | 2018-01-26 | |
| | | |||
* | | Experimental fix for #220. | 2018-01-15 | |
| | | |||
| * | Make coq-prog-args safe when list of strings. | 2017-12-22 | |
| | | | | | | | | They could be passed through _CoqProject regardless. | ||
* | | Fix #214. | 2017-12-11 | |
| | | | | | | | | If this works we should probably change the generic function as well. | ||
* | | Prettier cheat face (background + box). | 2017-11-06 | |
| | | |||
* | | Fix #135. | 2017-11-06 | |
| | | |||
* | | Limited extensibility of smie token detection. | 2017-10-26 | |
|/ | |||
* | changed -emacs-U flag to -emacs | 2017-07-19 | |
| | |||
* | Fixing a bug with Set/Unset commands due to recent commits. | 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. | 2017-06-06 | |
| | | | | | Checking whether the backtrack is inside a proof or not is a bit convoluted but seems ok. | ||
* | Merge pull request #185 from psteckler/remove-contribs | 2017-05-25 | |
|\ | | | | | Remove mmm and ML4PG contribs | ||
| * | Remove mmm and ML4PG contribs and remove references to them in code and docs | 2017-05-24 | |
| | | |||
* | | Fixing #183. | 2017-05-23 | |
|/ | |||
* | Fixing Set/Unset Printing broken by auto "Show". | 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. | 2017-05-12 | |
| | |||
* | Change (eval-when (compile) ...) to (eval-when-compile ...) | 2017-05-05 | |
| | | | | This fixes a bunch of compilation warnings | ||
* | Merge pull request #157 from ProofGeneral/elpa | 2017-05-05 | |
|\ | | | | | [WIP] ELPA/MELPA support | ||
* | | Typo from commit 758e679e. | 2017-04-25 | |
| | | |||
* | | Preparing new warning tags (no more special chars). | 2017-04-24 | |
| | | |||
* | | Fix #176. | 2017-04-19 | |
| | | | | | | | | | | The code uses several token searcher and the wrong one was called somewhere. | ||
* | | Fixing #173. | 2017-03-31 | |
| | | |||
* | | Added support for future new options (trunk). | 2017-03-22 | |
| | |