| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2012-06-04 | One more fix for indentation. | Pierre Courtieu | |
| 2012-06-04 | Fixing indentation (same bug than 2 previous commits). this time it seems ok. | Pierre Courtieu | |
| 2012-06-04 | Fixing the last fix on indentation. Still not perfect. | Pierre Courtieu | |
| 2012-06-03 | Fix a bug of indentation. | Pierre Courtieu | |
| 2012-05-31 | Fix of a bug. coq id can start with underscore. | Pierre Courtieu | |
| 2012-05-29 | - erase invalid coq-load-path entry format '("dir") | Hendrik Tews | |
| - check if coq-load-path is well-formed - update documentation | |||
| 2012-05-26 | another hide additional subgoals fix | Hendrik Tews | |
| 2012-05-24 | fix "Hide Additional Subgoals" for coq 8.4beta | Hendrik Tews | |
| 2012-05-09 | fix typo + add one missing cvsignore | Hendrik Tews | |
| 2012-02-13 | fix coqdep error recognition | Hendrik Tews | |
| 2012-02-10 | Fixed an ineficiency in comment detection. | Pierre Courtieu | |
| 2012-02-01 | Cleaning some code. | Pierre Courtieu | |
| 2012-02-01 | Quick fix of a regression introduced by my last commit. Looking for a | Pierre Courtieu | |
| better fix. | |||
| 2012-02-01 | Fixed command end recognition in presence of operators of the form .+ | Pierre Courtieu | |
| +. is not accepted yet. | |||
| 2012-01-18 | Fixed a small bug in indentation (ter repetita). Bullets are indented | Pierre Courtieu | |
| correctly provided that the precedence - > + > * is respected. | |||
| 2012-01-18 | Fixed a small bug in indentation (bis repetita). | Pierre Courtieu | |
| 2012-01-18 | Fixed a small bug in indentation. | Pierre Courtieu | |
| 2012-01-10 | Support proof-shell-interactive-prompt-regexp, ref Trac #430 | David Aspinall | |
| 2012-01-09 | proof-shell-start-goals-regexp: shy match to avoid introducing match group | David Aspinall | |
| 2012-01-04 | * fix case where some existential is instantiated with the last proof command | Hendrik Tews | |
| * protocol change - rename proof-complete into proof-finished and add existential info - add proof-complete message | |||
| 2012-01-03 | hide the dependent evars line | Hendrik Tews | |
| 2012-01-03 | merge ProofTreeBranch into main trunk: | Hendrik Tews | |
| - add support for proof-tree displays (currently Coq only) - new file generic/proof-tree.el contains generic code - Coq specific code has been added to coq/coq.el Changes to existing Proof General functions: - proof-shell-exec-loop and proof-shell-filter-manage-output call proof-tree display functions, when the proof-tree display is on - proof-shell-exec-loop returns t if proof-action-list is empty _or_ contains only items for updating the proof-tree - proof-shell-should-be-silent returns nil when the proof-tree display is on - coq-last-prompt-info, coq-last-prompt-info-safe return as additional 4th element the name of the current proof | |||
| 2011-12-27 | Extra test | David Aspinall | |
| 2011-12-27 | Typo | David Aspinall | |
| 2011-12-16 | Fixed some regexp. One for goal closing detection and one for | Pierre Courtieu | |
| understanding the new message about dependent evars (the two window mode was bugged). | |||
| 2011-12-16 | Adapting coq syntax recognition to the future v8.4 behavior of bullets | Pierre Courtieu | |
| (stand-alone commands), which is different of the experiments made until now in coq/trunk. | |||
| 2011-12-07 | - protect proof-shell-handle-delayed-output against the case where | Hendrik Tews | |
| proof-shell-end-goals-regexp is defined but does not match - add coq setting for hiding additional subgoals | |||
| 2011-12-06 | ensure optim-resp-window does not change the current buffer | Hendrik Tews | |
| 2011-12-05 | Applied a patch from Tom Prince which makes | Pierre Courtieu | |
| coq-update-minor-mode-alist behavior more acceptable. | |||
| 2011-11-15 | Quick stab at support for switching to proof shell when interactive support ↵ | David Aspinall | |
| expected, see Trac #430 | |||
| 2011-11-14 | Small fixes to coq smie indentation. | Pierre Courtieu | |
| 2011-11-11 | Fixed coq smie indentation. | Pierre Courtieu | |
| 2011-11-10 | Fixed coq smie indentation. | Pierre Courtieu | |
| 2011-11-10 | fixed some small bugs in coq indentation smie code. | Pierre Courtieu | |
| 2011-11-08 | added utf8 quantifiers for indentation + small fix in indentation. | Pierre Courtieu | |
| 2011-11-07 | Fixing syntax. | Pierre Courtieu | |
| 2011-11-07 | Fixed a bit more smie coq indentation. Still unfinished but useable. | Pierre Courtieu | |
| 2011-11-05 | Fixed several more bugs in smie indentation code. Not finished. | Pierre Courtieu | |
| 2011-11-04 | slowly fixing the last small bugs in smie indentation. | Pierre Courtieu | |
| 2011-11-04 | Fix previous commit (again). | Pierre Courtieu | |
| 2011-11-04 | Fix previous commit. | Pierre Courtieu | |
| 2011-11-03 | * coq.el (coq-smie-forward-token): Simplify by delegating to backward-token. | Stefan Monnier | |
| (coq-smie-backward-token): Use memq and member. | |||
| 2011-11-03 | Fixed the indentation of different kinds of use of the with keyword. | Pierre Courtieu | |
| 2011-11-02 | Added bullet indentation in smie code. smie code still needs some | Pierre Courtieu | |
| fixing to be be switched on. | |||
| 2011-10-17 | Attempt to support stricter bytecomp flags | David Aspinall | |
| 2011-10-03 | Update dates and versions | David Aspinall | |
| 2011-10-03 | Move a comment to docstring | David Aspinall | |
| 2011-09-23 | fix coqdep warning treated as error (library occurring at | Hendrik Tews | |
| multiple places in load-path) | |||
| 2011-09-15 | fix widget descriptions of coq-load-path | Hendrik Tews | |
| 2011-09-15 | -add support for -R and -I -as in coq-load-path | Hendrik Tews | |
| -improve documentation (and reorder stuff) | |||
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |