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