aboutsummaryrefslogtreecommitdiff
path: root/coq/coq.el
AgeCommit message (Expand)Author
2018-12-26Make coq-mode work without generic/proof-*Stefan Monnier
2018-12-22* coq-mode.el: New file to make coq-mode independent from PGStefan Monnier
2018-12-20Merge branch 'master' of github.com:ProofGeneral/PGPierre Courtieu
2018-12-20Fixes #395: hyps highlight is transient and with gray background.Pierre Courtieu
2018-12-19Quote ?( ?)soraros
2018-12-15Cosmetic cleanup of coq-smie, coq-syntax, and coq-abbrev.Stefan Monnier
2018-12-15Prepend cl- to more c[ad]+r instancesClément Pit-Claudel
2018-12-15Use cl-caddr instead of caddrClément Pit-Claudel
2018-12-13Use `cl-lib` instead of `cl` everywhereStefan Monnier
2018-12-12Cleanup patch; Moving defvar to toplevelStefan Monnier
2018-08-23Fix most doc issues raised by (checkdoc)Erik Martin-Dorel
2018-08-07Add coq-Print-Ltac to print an Ltac termJohn Grosen
2018-06-13small fix on hyp overlays.Pierre Courtieu
2018-06-13Fix multiple hyp overlays.Pierre Courtieu
2018-06-13Fix the fix #355.Pierre Courtieu
2018-06-11Small bug unhighlighting.Pierre Courtieu
2018-06-11key maps + small glitch hyp highlight/folding code.Pierre Courtieu
2018-06-08Changed the look of folding/unfolding hyps.Pierre Courtieu
2018-06-04Shorter CHANGES + smal fixes in hide/highlight hyps code.Pierre Courtieu
2018-06-01Click hypothesis to (un)hide them.Pierre Courtieu
2018-06-01Fixed a typo in previous commits.Pierre Courtieu
2018-05-31Infrastructure for hypothesis hiding.Pierre Courtieu
2018-05-31Fixing infrastructure for hypothesis highlighting.Pierre Courtieu
2018-05-31Infrastructure for transient hyps highlighting.Pierre Courtieu
2018-03-03Fix typos in custom variable descriptions. (#236)Tej Chajed
2018-02-21Update copyright messages and improve the header of elisp files.Erik Martin-Dorel
2017-12-11Fix #214.Pierre Courtieu
2017-06-08Fixing a bug with Set/Unset commands due to recent commits.Pierre Courtieu
2017-06-06Adding a Set Silent + Show when backtracking into a proof.Pierre Courtieu
2017-05-24Remove mmm and ML4PG contribs and remove references to them in code and docsPaul Steckler
2017-05-16Fixing Set/Unset Printing broken by auto "Show".Pierre Courtieu
2017-05-12temporary fix of automatic intros.Pierre Courtieu
2017-05-05Change (eval-when (compile) ...) to (eval-when-compile ...)Clément Pit--Claudel
2017-05-05Merge pull request #157 from ProofGeneral/elpaClément Pit-Claudel
2017-04-24Preparing new warning tags (no more special chars).Pierre Courtieu
2017-03-22Added support for future new options (trunk).Pierre Courtieu
2017-03-08Add a FIXME in coq.elClément Pit--Claudel
2017-03-08Remove compile-time calls to proof-ready-for-assistantClément Pit--Claudel
2017-03-08Remove unnecessary calls to 'eval-and-compile'Clément Pit--Claudel
2017-03-08Fix incorrect uses of defvarClément Pit--Claudel
2017-03-06get threeb frames only when neededPaul Steckler
2017-03-06one more redundant call removedPaul Steckler
2017-03-06remove redundant calls, simplify codePaul Steckler
2017-03-03Refreshing goal when Set Printing xxx. (#162)Pierre Courtieu
2017-02-23Fixing #154.Pierre Courtieu
2017-01-19save settings not defined with defpacustom (fixes #142)Hendrik Tews
2017-01-14Fix prooftree for Coq 8.6Hendrik Tews
2016-12-31add second argument to looking-back, required in emacs25Hendrik Tews
2016-12-28properly reset the vio2vo delay timerHendrik Tews
2016-12-15add quote to fix commit e3cc66dc2e60683531d75c12256d059ccbc64576Hendrik Tews
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 09:32:16 +0000