| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-03-13 | Summary: Revert change to default EMACS | David Aspinall | |
| 2015-03-13 | (fixes last commit) Added a command to send Queries to coq, with completion ↵ | Pierre Courtieu | |
| (C-c C-a C-q). Should replace C-c C-v at some point. Needs to have a complete list of such queries. Obeys C-u prefix for Printing all flag. | |||
| 2015-03-13 | Added a command to send Queries to coq, with completion (C-c C-a C-q). | Pierre Courtieu | |
| Should replace C-c C-v at some point. Needs to have a complete list of such queries. Obeys C-u prefix for Printing all flag. | |||
| 2015-03-11 | Summary: Update version year | David Aspinall | |
| 2015-03-11 | Summary: Build in default path for Isabelle2014 Mac package | David Aspinall | |
| 2015-03-09 | Added bug fixes in CHANGES. | Pierre Courtieu | |
| 2015-03-09 | Fixes #503. | Pierre Courtieu | |
| Added a "stop silent" if needed in proof-add-queue. This allows to recover verbosity when an error left the prover in silent mode. | |||
| 2015-03-05 | Fixed stuff in CHANGES. | Pierre Courtieu | |
| 2015-03-05 | Customization variables for modules, section and proof indentation. | Pierre Courtieu | |
| 2015-03-05 | Summary: Fix compile warning on phox-toolbar-entries | David Aspinall | |
| 2015-03-05 | Summary: Fix compile warning on isar-markup-ml | David Aspinall | |
| 2015-03-05 | Fix compile error with make-face | David Aspinall | |
| 2015-03-05 | Summary: Remove obsolete function | David Aspinall | |
| 2015-03-05 | Summary: Build on Mac | David Aspinall | |
| 2015-03-05 | Fix colours for dark backgrounds | David Aspinall | |
| 2015-03-04 | Fixed Proof end/start detection on Proof using ... | Pierre Courtieu | |
| Was making scripting confused. P. | |||
| 2015-03-04 | Fixed compilation issue with previous commit + CHANGE updates. | Pierre Courtieu | |
| 2015-03-03 | Mouse queries. | Pierre Courtieu | |
| If enabled, allows to send queries to coq with (control/shift/control-shift) mouse-1. | |||
| 2015-03-03 | Coqtop always restarted when switching script buffer. | Pierre Courtieu | |
| This comes from Hendrik's compile mode and is actually needed even when this mode is off. When switching scripting buffer, restart the coq shell process, so that it applies local coqtop options. | |||
| 2015-02-24 | Making freeze buffer hace coq-response-more. | Pierre Courtieu | |
| So that shortcuts work from this buffer. + colorizing. | |||
| 2015-02-23 | Typo in last commit. | Pierre Courtieu | |
| 2015-02-23 | Fixed 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-11 | Fixed 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-09 | replug removal of induction principle in SearAbout queries. | Pierre Courtieu | |
| 2015-02-09 | Adding 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-06 | Removed a debugging message. | Pierre Courtieu | |
| 2015-02-05 | Fix colorization of for coq multiple hypothesis on the same line. | Pierre Courtieu | |
| 2015-02-04 | cleaned previous commits (generic variable to disable error coloring). | Pierre Courtieu | |
| 2015-02-04 | Fixed previous commit (wrong regexp). | Pierre Courtieu | |
| 2015-02-03 | coloring names in resposne and goals | Pierre Courtieu | |
| 2015-02-03 | beautified a bit error messages. | Pierre Courtieu | |
| 2015-02-03 | cleaning regexp. | Pierre Courtieu | |
| 2015-02-02 | Fix test defeated by binary install | David Aspinall | |
| 2015-02-02 | Set version tag for new release. | David Aspinall | |
| 2015-01-30 | Set double hit electric terminator back. Disabled by default. | Pierre Courtieu | |
| 2015-01-27 | Fix coq project parsing and interpreting for coq v8.5. | Pierre Courtieu | |
| 2015-01-27 | Fixed a bug in script navigation. Updated CHANGE | Pierre Courtieu | |
| 2015-01-14 | changed default indentation of match's cases. | Pierre Courtieu | |
| 2015-01-09 | failed and commented attempt at improving indentation of records. | Pierre Courtieu | |
| 2015-01-09 | Removing non-smie indentation + fix CHANGES. | Pierre Courtieu | |
| 2015-01-05 | Fixing indentation of pending curly braces. | Pierre Courtieu | |
| 2015-01-05 | Fix compile on 23.x | David Aspinall | |
| 2015-01-05 | Fix crossref broken by newline. Remove custom font | David Aspinall | |
| 2015-01-05 | Set version tag for new release. | David Aspinall | |
| 2015-01-05 | Improvements for type tokens, remove preceding colon | David Aspinall | |
| 2015-01-05 | Fix haskell invocation comand | David Aspinall | |
| 2015-01-05 | Deleted file | David Aspinall | |
| 2015-01-05 | trying to indent pending forall in the expected way | Pierre Courtieu | |
| 2014-12-30 | removed debug message. | Pierre Courtieu | |
| 2014-12-30 | fixed indentation (lexing of 'with') + made local coq-load-path. | Pierre Courtieu | |
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |