aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq.el
Commit message (Expand)AuthorAge
* improve docGravatar Hendrik Tews2013-04-19
* - implement retract from prooftreeGravatar Hendrik Tews2013-01-20
* Fixed a bug with window height optimization.Gravatar Pierre Courtieu2013-01-17
* - support Grab Existential Variables for ProoftreeGravatar Hendrik Tews2013-01-17
* - support bullets and braces in ProoftreeGravatar Hendrik Tews2013-01-15
* - first version of parallel asynchronous compilation for coq inGravatar Hendrik Tews2012-11-13
* move coq compilation into coq/coq-seq-compile.elGravatar Hendrik Tews2012-10-30
* "as" insertion on a region.Gravatar Pierre Courtieu2012-10-03
* Fixed auto-insert-as stuff + fix compiling problems.Gravatar Pierre Courtieu2012-10-03
* Made 'as' automatic insertion a togglable feature (not finished) (2).Gravatar Pierre Courtieu2012-10-02
* Made 'as' automatic insertion a togglable feature. Not finished.Gravatar Pierre Courtieu2012-10-02
* Fixed 'as' close automatic insertion.Gravatar Pierre Courtieu2012-10-02
* Fixed the coq-insert-as feature. Will only work on coq svn trunk forGravatar Pierre Courtieu2012-10-01
* Fixed #419: coq synchronized variables are not anymore in the settingsGravatar Pierre Courtieu2012-09-25
* Completing the possible layouts of proof-layout-windows (added the 3Gravatar Pierre Courtieu2012-09-24
* coq-remove-trailing-dot: Fix accidental dynamic binding so it compilesGravatar David Aspinall2012-09-14
* adjust proof-tree regexp for focused subgoalsGravatar Hendrik Tews2012-09-14
* treat #450 by requiring that proofs are started with ProofGravatar Hendrik Tews2012-09-12
* Fix of the last commit.Gravatar Pierre Courtieu2012-09-07
* Fix a bug that was letting "." in a wrong syntax category.Gravatar Pierre Courtieu2012-09-07
* Cleaning code and comments.Gravatar Pierre Courtieu2012-09-07
* Fixed a bug with coq symbol detection at point. Now dot notation.are supported.Gravatar Pierre Courtieu2012-09-07
* Fixed double hit terminator. Now it is disabled by default, andGravatar Pierre Courtieu2012-09-05
* Fixing a bug happening in coq when three win mode on and scriptingGravatar Pierre Courtieu2012-08-31
* Resize response window when showing an ancient goal.Gravatar Pierre Courtieu2012-08-31
* Fixing previous commit on double hit.Gravatar Pierre Courtieu2012-08-31
* Impementing a "double hit" electric terminator. Idea: do electricGravatar Pierre Courtieu2012-08-30
* Summary: Don't quote lambda expressionsGravatar Stefan Monnier2012-08-30
* Added some new behavior to the usual 'show goal' shortcut: if point isGravatar Pierre Courtieu2012-08-30
* coq-optimise-resp-windows: Check proof script buffer window exists, addressin...Gravatar David Aspinall2012-08-09
* Rename optim-resp-windows -> coq-optimise-resp-windows for naming conventionGravatar David Aspinall2012-08-09
* Cleaned up a obsolete regexp.Gravatar Pierre Courtieu2012-07-25
* Making better menus for Coq. Menus visible in response and goals buffer.Gravatar Pierre Courtieu2012-07-22
* Fixed some regexp for V8.4 final version.Gravatar Pierre Courtieu2012-07-21
* Fixed widow shrinking hooks + added coq command shortcuts inGravatar Pierre Courtieu2012-07-19
* Adapted to late coq-8.4 new messages.Gravatar Pierre Courtieu2012-07-10
* Fixed incorrect syntax of previous commit.Gravatar Pierre Courtieu2012-07-10
* Made "printing all" queries smater in letting the prover in the sameGravatar Pierre Courtieu2012-07-10
* Fixing previous commit (Added completion to insert Require, based onGravatar Pierre Courtieu2012-07-09
* Added completion to insert Require, based on coq-load-path.Gravatar Pierre Courtieu2012-07-09
* Fixed a small bug in indentation + added new commands for queries withGravatar Pierre Courtieu2012-07-09
* Complete rework of the indentation mechanism using smie. The firstGravatar Pierre Courtieu2012-06-28
* Trying to minimize the slowness of indentation when no "Proof." isGravatar Pierre Courtieu2012-06-11
* Fixing indentation details for coq. All known bugs seems fixed.Gravatar Pierre Courtieu2012-06-10
* Fixing indentation details for coq.Gravatar Pierre Courtieu2012-06-10
* Still fixing indentation details for coq.Gravatar Pierre Courtieu2012-06-10
* Still fixing indentation (operator precedences) details for coq.Gravatar Pierre Courtieu2012-06-10
* Still fixing indentation details for coq.Gravatar Pierre Courtieu2012-06-10
* Made a small change in generic code about the setting ofGravatar Pierre Courtieu2012-06-09
* Indentation is a bit more accurate.Gravatar Pierre Courtieu2012-06-08
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-21 20:55:05 +0000