aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2015-02-23Fixed a bug in syntax table making fontlock and indentation fail.Pierre Courtieu
After some command detecting things at point, the indentation was broken.
2015-02-11Fixed read-only error for compile before require option.Pierre Courtieu
the emacs bug seems solved: the error with read-only always occur whatever locale is used. So I toggle read-only off in coq-compile-response.
2015-02-09replug removal of induction principle in SearAbout queries.Pierre Courtieu
2015-02-09Adding function to grab things at point and send queries about it.Pierre Courtieu
No shortcut yet but I am testing some "one click" stuff right now.
2015-02-06Removed a debugging message.Pierre Courtieu
2015-02-05Fix colorization of for coq multiple hypothesis on the same line.Pierre Courtieu
2015-02-04cleaned previous commits (generic variable to disable error coloring).Pierre Courtieu
2015-02-04Fixed previous commit (wrong regexp).Pierre Courtieu
2015-02-03coloring names in resposne and goalsPierre Courtieu
2015-02-03beautified a bit error messages.Pierre Courtieu
2015-02-03cleaning regexp.Pierre Courtieu
2015-02-02Fix test defeated by binary installDavid Aspinall
2015-02-02Set version tag for new release.David Aspinall
2015-01-30Set double hit electric terminator back. Disabled by default.Pierre Courtieu
2015-01-27Fix coq project parsing and interpreting for coq v8.5.Pierre Courtieu
2015-01-27Fixed a bug in script navigation. Updated CHANGEPierre Courtieu
2015-01-14changed default indentation of match's cases.Pierre Courtieu
2015-01-09failed and commented attempt at improving indentation of records.Pierre Courtieu
2015-01-09Removing non-smie indentation + fix CHANGES.Pierre Courtieu
2015-01-05Fixing indentation of pending curly braces.Pierre Courtieu
2015-01-05Fix compile on 23.xDavid Aspinall
2015-01-05Fix crossref broken by newline. Remove custom fontDavid Aspinall
2015-01-05Set version tag for new release.David Aspinall
2015-01-05Improvements for type tokens, remove preceding colonDavid Aspinall
2015-01-05Fix haskell invocation comandDavid Aspinall
2015-01-05Deleted fileDavid Aspinall
2015-01-05trying to indent pending forall in the expected wayPierre Courtieu
2014-12-30removed debug message.Pierre Courtieu
2014-12-30fixed indentation (lexing of 'with') + made local coq-load-path.Pierre Courtieu
2014-12-24fixed a bug in command parsing for coq, due to recent changes.Pierre Courtieu
2014-12-24typo in indentation cod, found after testing coq/ex/indent.v.Pierre Courtieu
2014-12-24fixing a small pb in indentation of arrow (->). Not perfect.Pierre Courtieu
2014-12-24fixed the use of >= 24.4 function string-suffix-p.Pierre Courtieu
2014-12-23Supporting more bullets (coq 8.5), like ++ or ++++.Pierre Courtieu
2014-12-23Fix a special case in _CoqProject syntax (empty string).Pierre Courtieu
2014-12-23Refix prettify compilation bug.Pierre Courtieu
2014-12-23fixed comilation of prettify setting.Pierre Courtieu
2014-12-22Fixed a compilation issue + small display glitch in coqpgPierre Courtieu
2014-12-22Fixing a bug of multiple frame mode (obsolete variable in emacs > 23.4.Pierre Courtieu
2014-12-18Fixed response display spurious newlines for coq.Pierre Courtieu
Added an option about that in proof-config. To check: I adapted proof-treee regrexp accordingly.
2014-12-16Remove trailing space in info messages in coq mode.Pierre Courtieu
2014-12-16Added a way to print eager message without warning face.Pierre Courtieu
It is the only way I found to display informativemessage appearing *before* the goal.
2014-12-09make name filtering of searchabout more precise.Pierre Courtieu
2014-12-09Added a variant of searchAbout hiding some spurious entries.Pierre Courtieu
2014-06-06Don't mess with overlay priorities.Stefan Monnier
2014-06-06* coq/coq-smie.el: Fix precedence of 'else'.Stefan Monnier
2014-06-04* coq-smie.el (coq-smie-.-deambiguate): Proofs don't start with a definition.Stefan Monnier
(coq-smie-backward-token): Don't burp at EOB. (coq-smie-rules): Indent top-level ":" like ":=".
2014-06-03Rename coq-smie-lexer.el to coq-smie.el.Stefan Monnier
2014-06-02* coq.el (coq-prettify-symbols-alist): New var.Stefan Monnier
(coq-mode-config): Use it.
2014-06-02* pg-response.el (proof-multiple-frames-enable, proof-next-error): Use newStefan Monnier
display-buffer-alist infrastructure if available.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 18:57:16 +0000