aboutsummaryrefslogtreecommitdiff
path: root/coq/coq.el
AgeCommit message (Expand)Author
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
2016-12-15fix :get for coq-search-blacklistHendrik Tews
2016-12-15Merge pull request #101 from tchajed/print-universes-optionhendriktews
2016-11-30fix customize-group coqHendrik Tews
2016-08-15Add Set Printing Universes to options menuTej Chajed
2016-08-14Replace "Set Implicit Arguments" option with "Set Printing Implicit".Erik Martin-Dorel
2016-06-23Coq: option to prefer top over bottom of concl.Pierre Courtieu
2016-05-20Merge branch 'master' of github.com:ProofGeneral/PGPierre Courtieu
2016-05-20Fix #72+ make user keywords prioritized over default ones.Pierre Courtieu
2016-05-16Merge branch 'master' of github.com:ProofGeneral/PGClément Pit--Claudel
2016-05-16Don't offer "" as the default in C-c C-c C-aClément Pit--Claudel
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:12:55 +0000