aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq.el
Commit message (Expand)AuthorAge
* 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
* fix :get for coq-search-blacklistGravatar Hendrik Tews2016-12-15
* Merge pull request #101 from tchajed/print-universes-optionGravatar hendriktews2016-12-15
|\
* | fix customize-group coqGravatar Hendrik Tews2016-11-30
| * Add Set Printing Universes to options menuGravatar Tej Chajed2016-08-15
|/
* Replace "Set Implicit Arguments" option with "Set Printing Implicit".Gravatar Erik Martin-Dorel2016-08-14
* Coq: option to prefer top over bottom of concl.Gravatar Pierre Courtieu2016-06-23
* Merge branch 'master' of github.com:ProofGeneral/PGGravatar Pierre Courtieu2016-05-20
|\
* | Fix #72+ make user keywords prioritized over default ones.Gravatar Pierre Courtieu2016-05-20
| * Merge branch 'master' of github.com:ProofGeneral/PGGravatar Clément Pit--Claudel2016-05-16
| |\ | |/ |/|
| * Don't offer "" as the default in C-c C-c C-aGravatar Clément Pit--Claudel2016-05-16
* | Merge branch 'master' of github.com:ProofGeneral/PGGravatar Pierre Courtieu2016-05-02
|\|