aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq
Commit message (Collapse)AuthorAge
* Cleanup patch; Moving defvar to toplevelGravatar Stefan Monnier2018-12-12
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Move `defvar`s used to silence warnings outside of eval-when-compile. Make sure they don't actually give a value to the var. * pg-init.el: Simplify. Use (if t ...) to avoid running `require` at compile-time. Don't add subdirs to load-path here since this code is never used. (pg-init--script-full-path, pg-init--pg-root): Inline their definition into their sole user. * generic/proof-utils.el (proof-resize-window-tofit): Inline definitions of window-leftmost-p and window-rightmost-p previously in proof-compat.el. * lib/proof-compat.el (proof-running-on-win32): Remove, not used. (mac-key-mode): Remove, there's no carbon-emacs-package-version in Emacs≥24.3. (pg-custom-undeclare-variable): Use dolist. (save-selected-frame): Remove, save-selected-window also saves&restores the selected frame at the same time. Update all users (which already used save-selected-window around it). (window-leftmost-p, window-rightmost-p, window-bottom-p) (find-coding-system): Remove, unused. * hol-light/hol-light.el (caml-font-lock-keywords): Don't try to defvar it to a dummy value and... (hol-light): ...check its existence before using it instead. * coq/coq.el (coq-may-use-prettify): Simplify initialization.
* Ignore ephemeral buffers, and buffers not pointed at files.Gravatar Calvin Beck2018-11-01
| | | | | | This helps with, for example, org-src-fontification buffers. https://lists.gnu.org/archive/html/emacs-orgmode/2016-03/msg00354.html
* Use non-remote path to expand paths in _CoqProject when file is remote.Gravatar Daniel Patterson2018-10-30
| | | | | | | | | When editing a remote file, the `coqtop` process will itself be remote, which means that the paths that are passed to it should be _local_, not remote. Otherwise, paths like '/ssh:hostname:/path/to/dir' get passed to `coqtop`, which has no idea what's going on. This relates to #203.
* Fix parsing of -arg in _CoqProject fileGravatar Anton Trunov2018-09-27
| | | | | The result of parsing was in reverse, see https://github.com/ProofGeneral/PG/issues/392\#issuecomment-425227314
* Fix most doc issues raised by (checkdoc)Gravatar Erik Martin-Dorel2018-08-23
|
* Merge pull request #379 from tchajed/variant-keywordGravatar Clément Pit-Claudel2018-08-21
|\ | | | | Support the Variant vernacular
* \ Merge branch 'master' of github.com:ProofGeneral/PGGravatar Pierre Courtieu2018-08-18
|\ \
* | | Fix #7980, keep option order unchanged.Gravatar Pierre Courtieu2018-08-18
| | |
| | * Support the Variant vernacularGravatar Tej Chajed2018-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 termGravatar John Grosen2018-08-07
|/
* Fixing last commit.Gravatar Pierre Courtieu2018-06-15
|
* Fix #368 (emacs < 25 split-string has no trim arg).Gravatar Pierre Courtieu2018-06-15
| | | | Copied some code from company-coq.
* small fix on hyp overlays.Gravatar Pierre Courtieu2018-06-13
|
* Fix multiple hyp overlays.Gravatar Pierre Courtieu2018-06-13
| | | | | queries would trigger re-generarion of overlays. Now overlays are generated if there are no overlays already.
* Fix the fix #355.Gravatar Pierre Courtieu2018-06-13
| | | | The fix was bad: no ore hyps were foldable/highlightable.
* Small bug unhighlighting.Gravatar Pierre Courtieu2018-06-11
| | | | | Selecting the unhighlightied hyps showed a different region color. Setting the face to nil is better.
* fix #355 + probable bug.Gravatar Pierre Courtieu2018-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.Gravatar Pierre Courtieu2018-06-11
|
* Changed the look of folding/unfolding hyps.Gravatar Pierre Courtieu2018-06-08
|
* Small fix in a regexp.Gravatar Pierre Courtieu2018-06-06
|
* Shorter CHANGES + smal fixes in hide/highlight hyps code.Gravatar Pierre Courtieu2018-06-04
|
* Click hypothesis to (un)hide them.Gravatar Pierre Courtieu2018-06-01
|
* Fixed a typo in previous commits.Gravatar Pierre Courtieu2018-06-01
|
* Infrastructure for hypothesis hiding.Gravatar Pierre Courtieu2018-05-31
|
* Fixing infrastructure for hypothesis highlighting.Gravatar Pierre Courtieu2018-05-31
|
* Merge branch 'master' of github.com:ProofGeneral/PGGravatar Pierre Courtieu2018-05-31
|\
* | Infrastructure for transient hyps highlighting.Gravatar Pierre Courtieu2018-05-31
| |
| * small fix of face `coq-symbol-face'Gravatar stardiviner2018-04-22
| |
| * Merge pull request #207 from SkySkimmer/masterGravatar Erik Martin-Dorel2018-04-08
|/| | | | | Make coq-prog-args safe when list of strings.
* | Fix typos in custom variable descriptions. (#236)Gravatar Tej Chajed2018-03-03
| |
* | Update copyright messages and improve the header of elisp files.Gravatar Erik Martin-Dorel2018-02-21
| |
* | typo in abbrevs.Gravatar Pierre Courtieu2018-02-07
| |
* | look for vernac controls before focus bracket, fix for #223Gravatar Paul Steckler2018-01-26
| |
* | Experimental fix for #220.Gravatar Pierre Courtieu2018-01-15
| |
| * Make coq-prog-args safe when list of strings.Gravatar Gaëtan Gilbert2017-12-22
| | | | | | | | They could be passed through _CoqProject regardless.
* | Fix #214.Gravatar Pierre Courtieu2017-12-11
| | | | | | | | If this works we should probably change the generic function as well.
* | Prettier cheat face (background + box).Gravatar Pierre Courtieu2017-11-06
| |
* | Fix #135.Gravatar Pierre Courtieu2017-11-06
| |
* | Limited extensibility of smie token detection.Gravatar Pierre Courtieu2017-10-26
|/
* changed -emacs-U flag to -emacsGravatar Paul Steckler2017-07-19
|
* Fixing a bug with Set/Unset commands due to recent commits.Gravatar Pierre Courtieu2017-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.Gravatar Pierre Courtieu2017-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-contribsGravatar psteckler2017-05-25
|\ | | | | Remove mmm and ML4PG contribs
| * Remove mmm and ML4PG contribs and remove references to them in code and docsGravatar Paul Steckler2017-05-24
| |
* | Fixing #183.Gravatar Pierre Courtieu2017-05-23
|/
* Fixing Set/Unset Printing broken by auto "Show".Gravatar Pierre Courtieu2017-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.Gravatar Pierre Courtieu2017-05-12
|
* Change (eval-when (compile) ...) to (eval-when-compile ...)Gravatar Clément Pit--Claudel2017-05-05
| | | | This fixes a bunch of compilation warnings
* Merge pull request #157 from ProofGeneral/elpaGravatar Clément Pit-Claudel2017-05-05
|\ | | | | [WIP] ELPA/MELPA support
* | Typo from commit 758e679e.Gravatar Pierre Courtieu2017-04-25
| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 23:36:01 +0000