index
:
proof-general
master
Emacs interface for proof assistants
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
coq
/
coq-abbrev.el
Commit message (
Expand
)
Author
Age
*
Update copyright messages and improve the header of elisp files.
Erik Martin-Dorel
2018-02-21
*
Remove mmm and ML4PG contribs and remove references to them in code and docs
Paul Steckler
2017-05-24
*
Merge pull request #157 from ProofGeneral/elpa
Clément Pit-Claudel
2017-05-05
|
\
*
|
Added support for future new options (trunk).
Pierre Courtieu
2017-03-22
|
*
Remove uses of defpgdefault in coq-abbrev
Clément Pit--Claudel
2017-03-08
|
*
Fix incorrect assumption that noninteractive == byte-compiling
Clément Pit--Claudel
2017-03-08
|
/
*
save settings not defined with defpacustom (fixes #142)
Hendrik Tews
2017-01-19
*
Merge pull request #101 from tchajed/print-universes-option
hendriktews
2016-12-15
|
\
*
|
fix generic interrupt procedure to interrupt parallel background compilation
Hendrik Tews
2016-12-14
*
|
option coq-compile-keep-going for parallel compilation
Hendrik Tews
2016-12-08
*
|
reconcile menu for auto compilation
Hendrik Tews
2016-11-18
*
|
first version for quick compilation
Hendrik Tews
2016-11-16
|
*
Add Set Printing Universes to options menu
Tej Chajed
2016-08-15
|
/
*
Sort the OPTIONS menu items differently & Fix a typo (UnSet -> Unset).
Erik Martin-Dorel
2016-08-14
*
Replace "Set Implicit Arguments" option with "Set Printing Implicit".
Erik Martin-Dorel
2016-08-14
*
Adding an setting for Search Blacklist coq option.
Pierre Courtieu
2015-12-09
*
proof-assert-command-hook added + Auto adjust width in coq mode.
Pierre Courtieu
2015-10-12
*
A command to set coq printing width smartly.
Pierre Courtieu
2015-03-26
*
Added a command to send Queries to coq, with completion (C-c C-a C-q).
Pierre Courtieu
2015-03-13
*
Added a variant of searchAbout hiding some spurious entries.
Pierre Courtieu
2014-12-09
*
Fixing coq project file parsing + moved project options.
Pierre Courtieu
2013-07-22
*
ML4PG functionality added to Coq menu
joheras
2013-05-30
*
Fixed #419: coq synchronized variables are not anymore in the settings
Pierre Courtieu
2012-09-25
*
Added a menu to set the 3 windows layout.
Pierre Courtieu
2012-09-25
*
Fixed double hit terminator. Now it is disabled by default, and
Pierre Courtieu
2012-09-05
*
Changed the behaviour of proof-layout-windows. Now it follows the
Pierre Courtieu
2012-08-31
*
Making better menus for Coq. Menus visible in response and goals buffer.
Pierre Courtieu
2012-07-22
*
Added completion to insert Require, based on coq-load-path.
Pierre Courtieu
2012-07-09
*
Fixed a small bug in indentation + added new commands for queries with
Pierre Courtieu
2012-07-09
*
Summary: coq-smie: improve indentation.
Stefan Monnier
2011-06-07
*
Alternative fix to #382.
David Aspinall
2011-01-18
*
Fix trac 382 by not setting save-abbrevs.
Pierre Courtieu
2011-01-18
*
Fixed experimental feature of storing response or goal in a persistent
Pierre Courtieu
2010-09-01
*
Comments
David Aspinall
2009-09-08
*
Move holes menu to holes mode
David Aspinall
2009-09-06
*
Moved doc of holes to holes-mode
David Aspinall
2009-09-06
*
Clean whitespace
David Aspinall
2009-09-05
*
Changed the main menu of coq. Changed a shortcut for holes.
Pierre Courtieu
2008-07-21
*
Remove faulty test
David Aspinall
2008-07-05
*
Fixed a bug with abbrev table definition.
Pierre Courtieu
2008-05-22
*
Fixed a problem with a wrong side effect on syntax databases (when
Pierre Courtieu
2008-01-28
*
Many compatibility updates, bug fixes, rearrangements for compilation.
David Aspinall
2008-01-15
*
Fixed abbrev installation. + small fixes.
Pierre Courtieu
2008-01-03
*
Fix compilation problems and rearrange startup settings for coq-prog-name,coq...
David Aspinall
2007-12-14
*
Remove eval-when, seems unreliable
David Aspinall
2007-12-14
*
Attempt to fix compile problems
David Aspinall
2007-12-14
*
Added some unknown keyword (not changing state). Fixes bug 113 from emakarov.M
Pierre Courtieu
2007-04-26
*
Fixed a small bug in indentation of coq.
Pierre Courtieu
2006-08-25
*
Cleaning in coq and lib, fixed licenses and docstrings.
Pierre Courtieu
2006-08-23
*
Finished making functions over big tables non recursive. Works with
Pierre Courtieu
2006-08-23
[next]