aboutsummaryrefslogtreecommitdiff
path: root/coq
AgeCommit message (Collapse)Author
2012-10-03"as" insertion on a region.Pierre Courtieu
2012-10-03Fixed auto-insert-as stuff + fix compiling problems.Pierre Courtieu
2012-10-02Made 'as' automatic insertion a togglable feature (not finished) (2).Pierre Courtieu
2012-10-02Made 'as' automatic insertion a togglable feature. Not finished.Pierre Courtieu
2012-10-02Fixed 'as' close automatic insertion.Pierre Courtieu
2012-10-01Fixed the coq-insert-as feature. Will only work on coq svn trunk forPierre Courtieu
now. coq-8.4 not compatible.
2012-09-25Fixed #419: coq synchronized variables are not anymore in the settingsPierre Courtieu
menu, they are in option menu that only issues commands to the prover and do not try to keep track of the values of the variables.
2012-09-25Added a menu to set the 3 windows layout.Pierre Courtieu
2012-09-25Fixed indentation in presence of "dot friends" like :?. etc.Pierre Courtieu
2012-09-24Completing the possible layouts of proof-layout-windows (added the 3Pierre Courtieu
columns mode).
2012-09-21Fixing a bad interaction between one unicode token and electricPierre Courtieu
terminator.
2012-09-14coq-remove-trailing-dot: Fix accidental dynamic binding so it compilesDavid Aspinall
2012-09-14adjust proof-tree regexp for focused subgoalsHendrik Tews
2012-09-12treat #450 by requiring that proofs are started with ProofHendrik Tews
2012-09-07Fix of the last commit.Pierre Courtieu
2012-09-07Fix a bug that was letting "." in a wrong syntax category.Pierre Courtieu
2012-09-07Cleaning code and comments.Pierre Courtieu
2012-09-07Fixed a bug with coq symbol detection at point. Now dot notation.are supported.Pierre Courtieu
2012-09-06Fixed a bug with function name "eval" (end of).Pierre Courtieu
2012-09-06Fixed a bug with function name "eval".Pierre Courtieu
2012-09-05Fixed double hit terminator. Now it is disabled by default, andPierre Courtieu
enabling it disables electric-terminator and vice-versa. In case both are non nil at the same time, then electric teminator has priority. If people like it we may propose this to other modes than coq. + fixed window layout policy.
2012-09-02Remove ref to file parsingcheck-412.v missing from CVS, so "make ↵David Aspinall
coq.autotest" runs again
2012-08-31Changed the behaviour of proof-layout-windows. Now it follows thePierre Courtieu
'horizontal 'vertical 'smart policy.
2012-08-31Fixing a bug happening in coq when three win mode on and scriptingPierre Courtieu
starts on a buffer. The response buffer was hiding the scripting buffer. NOTE: this is not a bug correction. The bug is still there but proof-layout-windows is called to work it around.
2012-08-31Resize response window when showing an ancient goal.Pierre Courtieu
2012-08-31Fixing previous commit on double hit.Pierre Courtieu
2012-08-30Impementing a "double hit" electric terminator. Idea: do electricPierre Courtieu
terminator when hitting "." twice quickly.
2012-08-30Summary: Don't quote lambda expressionsStefan Monnier
* coq/coq-indent.el (coq-indent-inner-regexp): Remove old X-Symbol element. (coq-save-count, coq-proof-count): * obsolete/plastic/plastic.el (plastic-shell-handle-output): * lib/texi-docstring-magic.el (texi-docstring-magic-insert-magic): * lib/pg-dev.el (emacs-lisp-mode-hook): * lib/maths-menu.el (maths-menu-filter-predicate) (maths-menu-tokenise-insert): * lib/holes.el (holes-next): * lego/lego.el (lego-shell-handle-output): * isar/isabelle-system.el (isabelle-docs-menu): * coq/coq.el (coq-compile-command, coq-compile-auto-save) (coq-compile-ignored-directories, coq-load-path-safep) (proof-shell-handle-delayed-output-hook): Don't quote lambda.
2012-08-30Added some new behavior to the usual 'show goal' shortcut: if point isPierre Courtieu
on a locked span, it now displays the corresponding (ancient) goal instead of the current one.
2012-08-24Fixed an error when smie not present in the system.Pierre Courtieu
2012-08-16Fix lambda quoteDavid Aspinall
2012-08-09coq-optimise-resp-windows: Check proof script buffer window exists, ↵David Aspinall
addressing Trac #446
2012-08-09Rename optim-resp-windows -> coq-optimise-resp-windows for naming conventionDavid Aspinall
2012-07-25Cleaned up a obsolete regexp.Pierre Courtieu
2012-07-24Fixing compilation. Still need to verify some smie stuff on different ↵Pierre Courtieu
versions of emacs.
2012-07-22Making better menus for Coq. Menus visible in response and goals buffer.Pierre Courtieu
2012-07-21Fixed some regexp for V8.4 final version.Pierre Courtieu
2012-07-19Fixed widow shrinking hooks + added coq command shortcuts inPierre Courtieu
coq-response buffer.
2012-07-10Adapted to late coq-8.4 new messages.Pierre Courtieu
2012-07-10Fixed incorrect syntax of previous commit.Pierre Courtieu
2012-07-10Made "printing all" queries smater in letting the prover in the samePierre Courtieu
printing state as before.
2012-07-09Fixing previous commit (Added completion to insert Require, based onPierre Courtieu
coq-load-path) in the case of complex coq-load-path.
2012-07-09Added completion to insert Require, based on coq-load-path.Pierre Courtieu
2012-07-09Fixed a small bug in indentation + added new commands for queries withPierre Courtieu
Printing Implicit and Printing All flags.
2012-07-07Debugged coq indentation.Pierre Courtieu
2012-07-06More fixes in coq indentation (2).Pierre Courtieu
2012-07-06More fixes in coq indentation.Pierre Courtieu
2012-07-05Indentation debugging for coq.Pierre Courtieu
2012-07-05Code cleaning.Pierre Courtieu
2012-07-05Fixed some indentation details for Coq.Pierre Courtieu
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-19 11:09:38 +0000