aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq
Commit message (Expand)AuthorAge
* Added a menu to set the 3 windows layout.Gravatar Pierre Courtieu2012-09-25
* Fixed indentation in presence of "dot friends" like :?. etc.Gravatar Pierre Courtieu2012-09-25
* Completing the possible layouts of proof-layout-windows (added the 3Gravatar Pierre Courtieu2012-09-24
* Fixing a bad interaction between one unicode token and electricGravatar Pierre Courtieu2012-09-21
* 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 a bug with function name "eval" (end of).Gravatar Pierre Courtieu2012-09-06
* Fixed a bug with function name "eval".Gravatar Pierre Courtieu2012-09-06
* Fixed double hit terminator. Now it is disabled by default, andGravatar Pierre Courtieu2012-09-05
* Remove ref to file parsingcheck-412.v missing from CVS, so "make coq.autotest...Gravatar David Aspinall2012-09-02
* Changed the behaviour of proof-layout-windows. Now it follows theGravatar Pierre Courtieu2012-08-31
* 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
* Fixed an error when smie not present in the system.Gravatar Pierre Courtieu2012-08-24
* Fix lambda quoteGravatar David Aspinall2012-08-16
* 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
* Fixing compilation. Still need to verify some smie stuff on different version...Gravatar Pierre Courtieu2012-07-24
* 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
* Debugged coq indentation.Gravatar Pierre Courtieu2012-07-07
* More fixes in coq indentation (2).Gravatar Pierre Courtieu2012-07-06
* More fixes in coq indentation.Gravatar Pierre Courtieu2012-07-06
* Indentation debugging for coq.Gravatar Pierre Courtieu2012-07-05
* Code cleaning.Gravatar Pierre Courtieu2012-07-05
* Fixed some indentation details for Coq.Gravatar Pierre Courtieu2012-07-05
* Fixed a syntactic recognition function. Should Fix #2819.Gravatar Pierre Courtieu2012-07-05
* Fixed some indentation bugs.Gravatar Pierre Courtieu2012-07-03
* Fixed some small bugs in coq indentation.Gravatar Pierre Courtieu2012-06-28
* Complete rework of the indentation mechanism using smie. The firstGravatar Pierre Courtieu2012-06-28
* Simplified file variables code.Gravatar Pierre Courtieu2012-06-19
* Fix a bug in coq indet code when at the beginning of a buffer.Gravatar Pierre Courtieu2012-06-14
* Trying to minimize the slowness of indentation when no "Proof." isGravatar Pierre Courtieu2012-06-11
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 05:36:06 +0000