Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Fix most doc issues raised by (checkdoc) | Erik Martin-Dorel | 2018-08-23 |
| | |||
* | Merge pull request #379 from tchajed/variant-keyword | Clément Pit-Claudel | 2018-08-21 |
|\ | | | | | Support the Variant vernacular | ||
* \ | Merge branch 'master' of github.com:ProofGeneral/PG | Pierre Courtieu | 2018-08-18 |
|\ \ | |||
* | | | Fix #7980, keep option order unchanged. | Pierre Courtieu | 2018-08-18 |
| | | | |||
| | * | Support the Variant vernacular | Tej Chajed | 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 | John Grosen | 2018-08-07 |
|/ | |||
* | Fixing last commit. | Pierre Courtieu | 2018-06-15 |
| | |||
* | Fix #368 (emacs < 25 split-string has no trim arg). | Pierre Courtieu | 2018-06-15 |
| | | | | Copied some code from company-coq. | ||
* | 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. | ||
* | fix #355 + probable bug. | Pierre Courtieu | 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. | Pierre Courtieu | 2018-06-11 |
| | |||
* | Changed the look of folding/unfolding hyps. | Pierre Courtieu | 2018-06-08 |
| | |||
* | Small fix in a regexp. | Pierre Courtieu | 2018-06-06 |
| | |||
* | 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 |
| | |||
* | Merge branch 'master' of github.com:ProofGeneral/PG | Pierre Courtieu | 2018-05-31 |
|\ | |||
* | | Infrastructure for transient hyps highlighting. | Pierre Courtieu | 2018-05-31 |
| | | |||
| * | small fix of face `coq-symbol-face' | stardiviner | 2018-04-22 |
| | | |||
| * | Merge pull request #207 from SkySkimmer/master | Erik Martin-Dorel | 2018-04-08 |
|/| | | | | | Make coq-prog-args safe when list of strings. | ||
* | | 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 |
| | | |||
* | | typo in abbrevs. | Pierre Courtieu | 2018-02-07 |
| | | |||
* | | look for vernac controls before focus bracket, fix for #223 | Paul Steckler | 2018-01-26 |
| | | |||
* | | Experimental fix for #220. | Pierre Courtieu | 2018-01-15 |
| | | |||
| * | Make coq-prog-args safe when list of strings. | Gaëtan Gilbert | 2017-12-22 |
| | | | | | | | | They could be passed through _CoqProject regardless. | ||
* | | Fix #214. | Pierre Courtieu | 2017-12-11 |
| | | | | | | | | If this works we should probably change the generic function as well. | ||
* | | Prettier cheat face (background + box). | Pierre Courtieu | 2017-11-06 |
| | | |||
* | | Fix #135. | Pierre Courtieu | 2017-11-06 |
| | | |||
* | | Limited extensibility of smie token detection. | Pierre Courtieu | 2017-10-26 |
|/ | |||
* | changed -emacs-U flag to -emacs | Paul Steckler | 2017-07-19 |
| | |||
* | 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. | ||
* | Merge pull request #185 from psteckler/remove-contribs | psteckler | 2017-05-25 |
|\ | | | | | Remove mmm and ML4PG contribs | ||
| * | Remove mmm and ML4PG contribs and remove references to them in code and docs | Paul Steckler | 2017-05-24 |
| | | |||
* | | Fixing #183. | Pierre Courtieu | 2017-05-23 |
|/ | |||
* | 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 | ||
* | | Typo from commit 758e679e. | Pierre Courtieu | 2017-04-25 |
| | | |||
* | | Preparing new warning tags (no more special chars). | Pierre Courtieu | 2017-04-24 |
| | | |||
* | | Fix #176. | Pierre Courtieu | 2017-04-19 |
| | | | | | | | | | | The code uses several token searcher and the wrong one was called somewhere. | ||
* | | Fixing #173. | Pierre Courtieu | 2017-03-31 |
| | | |||
* | | Added support for future new options (trunk). | Pierre Courtieu | 2017-03-22 |
| | |