Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | 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 | |
| | | |||
| * | Add a FIXME in coq.el | 2017-03-08 | |
| | | |||
| * | Remove uses of defpgdefault in coq-abbrev | 2017-03-08 | |
| | | | | | | | | | | | | This file is `require'-d when compiling coq.el, and at that point the proof assistant isn't set to coq yet, so it would define variables prefixed by `nil-' instead of `coq'. | ||
| * | Remove uses of defpacustom in coq-compile-common | 2017-03-08 | |
| | | | | | | | | | | | | This file is `require'-d from other places, at compile time. This doesn't work nicely with compilation by package.el (PG complains and says "defpacustom: Proof assistant setting compile-before-require re-defined!") | ||
| * | Remove compile-time calls to proof-ready-for-assistant | 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' | 2017-03-08 | |
| | | |||
| * | Fix incorrect uses of defvar | 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. | ||
| * | Fix incorrect assumption that noninteractive == byte-compiling | 2017-03-08 | |
|/ | | | | | The PG Makefile does ensure (using --batch) that noninteractive is non-nil while compiling, but package.el doesn't. | ||
* | Merge commit '06fd76163b857a056ac44e7437efa17656f06e5b' | 2017-03-08 | |
|\ | |||
| * | Fixing unicode tokens in generic code and in coq. | 2017-03-08 | |
| | | |||
* | | get threeb frames only when needed | 2017-03-06 | |
| | |