aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq.el
Commit message (Expand)AuthorAge
* Make coq-mode work without generic/proof-*Gravatar Stefan Monnier2018-12-26
* * coq-mode.el: New file to make coq-mode independent from PGGravatar Stefan Monnier2018-12-22
* Merge branch 'master' of github.com:ProofGeneral/PGGravatar Pierre Courtieu2018-12-20
|\
* | Fixes #395: hyps highlight is transient and with gray background.Gravatar Pierre Courtieu2018-12-20
| * Quote ?( ?)Gravatar soraros2018-12-19
| * Cosmetic cleanup of coq-smie, coq-syntax, and coq-abbrev.Gravatar Stefan Monnier2018-12-15
| * Prepend cl- to more c[ad]+r instancesGravatar Clément Pit-Claudel2018-12-15
| * Use cl-caddr instead of caddrGravatar Clément Pit-Claudel2018-12-15
|/
* Use `cl-lib` instead of `cl` everywhereGravatar Stefan Monnier2018-12-13
* Cleanup patch; Moving defvar to toplevelGravatar Stefan Monnier2018-12-12
* Fix most doc issues raised by (checkdoc)Gravatar Erik Martin-Dorel2018-08-23
* Add coq-Print-Ltac to print an Ltac termGravatar John Grosen2018-08-07
* small fix on hyp overlays.Gravatar Pierre Courtieu2018-06-13
* Fix multiple hyp overlays.Gravatar Pierre Courtieu2018-06-13
* Fix the fix #355.Gravatar Pierre Courtieu2018-06-13
* Small bug unhighlighting.Gravatar Pierre Courtieu2018-06-11
* 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
* 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
* Infrastructure for transient hyps highlighting.Gravatar Pierre Courtieu2018-05-31
* 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
* Fix #214.Gravatar Pierre Courtieu2017-12-11
* Fixing a bug with Set/Unset commands due to recent commits.Gravatar Pierre Courtieu2017-06-08
* Adding a Set Silent + Show when backtracking into a proof.Gravatar Pierre Courtieu2017-06-06
* Remove mmm and ML4PG contribs and remove references to them in code and docsGravatar Paul Steckler2017-05-24
* Fixing Set/Unset Printing broken by auto "Show".Gravatar Pierre Courtieu2017-05-16
* 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
* Merge pull request #157 from ProofGeneral/elpaGravatar Clément Pit-Claudel2017-05-05
|\
* | Preparing new warning tags (no more special chars).Gravatar Pierre Courtieu2017-04-24
* | Added support for future new options (trunk).Gravatar Pierre Courtieu2017-03-22
| * Add a FIXME in coq.elGravatar Clément Pit--Claudel2017-03-08
| * Remove compile-time calls to proof-ready-for-assistantGravatar Clément Pit--Claudel2017-03-08
| * Remove unnecessary calls to 'eval-and-compile'Gravatar Clément Pit--Claudel2017-03-08
| * Fix incorrect uses of defvarGravatar Clément Pit--Claudel2017-03-08
|/
* get threeb frames only when neededGravatar Paul Steckler2017-03-06
* one more redundant call removedGravatar Paul Steckler2017-03-06
* remove redundant calls, simplify codeGravatar Paul Steckler2017-03-06
* Refreshing goal when Set Printing xxx. (#162)Gravatar Pierre Courtieu2017-03-03
* Fixing #154.Gravatar Pierre Courtieu2017-02-23
* save settings not defined with defpacustom (fixes #142)Gravatar Hendrik Tews2017-01-19
* Fix prooftree for Coq 8.6Gravatar Hendrik Tews2017-01-14
* add second argument to looking-back, required in emacs25Gravatar Hendrik Tews2016-12-31
* properly reset the vio2vo delay timerGravatar Hendrik Tews2016-12-28
* add quote to fix commit e3cc66dc2e60683531d75c12256d059ccbc64576Gravatar Hendrik Tews2016-12-15