| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-12-14 | Fixing coq-prog-arg for auto compilation. | Pierre Courtieu | |
| 2015-12-10 | Fixing variable declaration. | Pierre Courtieu | |
| 2015-12-09 | Adding an setting for Search Blacklist coq option. | Pierre Courtieu | |
| 2015-12-07 | Speeding up indentation (regexp optim). | Pierre Courtieu | |
| 2015-12-07 | Speeding up indentation. | Pierre Courtieu | |
| Dedicated regexp for bullets when searching backward. | |||
| 2015-12-05 | Fixed #15 + more speedup of indentation. | Pierre Courtieu | |
| Experimenting on more regexp and less adhoc searching in the smie lexer. In particular the regexp for bullet seems now capture only real bullets. | |||
| 2015-12-04 | Fixed a typo. | Pierre Courtieu | |
| 2015-11-30 | Speeding up indentation code (smie lexer). | Pierre Courtieu | |
| 2015-11-30 | Updated the CHANGES files, mainly git url. | Pierre Courtieu | |
| 2015-11-26 | A shortcut for coq-insert-as-in-next-command. | Pierre Courtieu | |
| Works well for a single induction/destruct. Works sometimes for inversion. Does not work in presence of eqn flag yet (easy to fix). Does not work on ;-combined tactics (hard to fix). Does not work on a lot of inversion invocation (but some are ok). We basically need another "as" tactical with a retro-predictable input. That is: when seeing the resulting goal we can deduce what would have been the right "as" close. This is currently the case only for destruct/induction !foo (notice the exclamation mark). | |||
| 2015-11-23 | Introduce a coq-question-mark-face | Clément Pit--Claudel | |
| Closes #12 | |||
| 2015-11-17 | recompilation: Improve error checking | Clément Pit--Claudel | |
| Bug recipe: * Process some imports * Enable on the fly compilation * Kill coq process Error: Debugger entered--Lisp error: (wrong-type-argument hash-table-p nil) maphash((lambda (ancestor state) (if (eq state (quote locked)) (progn (coq-unlock-ancestor ancestor) (puthash ancestor nil coq-par-ancestor-files)))) nil) (progn (maphash (function (lambda (ancestor state) (if (eq state (quote locked)) (progn (coq-unlock-ancestor ancestor) (puthash ancestor nil coq-par-ancestor-files))))) coq-par-ancestor-files)) (if (or t coq-par-ancestor-files) (progn (maphash (function (lambda (ancestor state) (if (eq state (quote locked)) (progn (coq-unlock-ancestor ancestor) (puthash ancestor nil coq-par-ancestor-files))))) coq-par-ancestor-files))) coq-par-unlock-ancestors-on-error() coq-par-emergency-cleanup() run-hooks(proof-shell-signal-interrupt-hook) proof-shell-kill-function() kill-buffer(#<buffer *coq*>) proof-shell-exit(nil) funcall-interactively(proof-shell-exit nil) #<subr call-interactively>(proof-shell-exit nil nil) ad-Advice-call-interactively(#<subr call-interactively> proof-shell-exit nil nil) apply(ad-Advice-call-interactively #<subr call-interactively> (proof-shell-exit nil nil)) call-interactively(proof-shell-exit nil nil) command-execute(proof-shell-exit) | |||
| 2015-11-13 | compilation fix (coq-pre-v85). | Pierre Courtieu | |
| 2015-11-13 | Experimenting less brutal frame deletion. | Pierre Courtieu | |
| Only in coq mode for now. There are still some strange frame deletion some times. | |||
| 2015-11-13 | Fixed auto-width setting not initialized (trac #456). | Pierre Courtieu | |
| 2015-11-13 | Cleaning code for auto width adapting. | Pierre Courtieu | |
| Less guessing, separate guessing code. | |||
| 2015-11-12 | Tentative fix for #10 | Clément Pit--Claudel | |
| 2015-11-12 | Close #9 | Clément Pit--Claudel | |
| 2015-11-12 | Debuging: display a warning. | Pierre Courtieu | |
| The warning is displayed when failing to retrieve last prompt info. Once we understand what happened we can remove this warning. | |||
| 2015-11-02 | coq-pre-v85 option to fix coqdep invocation in [compile before require]. | Pierre Courtieu | |
| Command line options changed heavily betwenn 8.4 and 8.5. We need an option to force V8.4 in some cases, mainly to infer the right coqtop/coqdep invocations. | |||
| 2015-10-20 | Re-thinking auto-insert-as. | Pierre Courtieu | |
| Now there is acommand that adds as close to the next to be scripted command. Finally found a way to make this close to correct for destruct and induction by using "!" modifier on the destructed names, so that the automatic naming does not reuse the this name. Probably still very approximated for inversion. | |||
| 2015-10-15 | Fixed the regexp for colorizing hyps in the goal. | Pierre Courtieu | |
| 2015-10-13 | Fixed coq-id-at-point. | Pierre Courtieu | |
| 2015-10-13 | proof-retract-command-hook added + more auto adjust width in coq mode. | Pierre Courtieu | |
| 2015-10-12 | proof-assert-command-hook added + Auto adjust width in coq mode. | Pierre Courtieu | |
| This hook was missing, it allows to send complete commands before the (set of) command(s) sent by the user. It shall be used when proof-shell-insert-hook cannot be used (because of multiple prompts appearing). | |||
| 2015-10-09 | Trying to not delete frames too eagerly when laying out. | Pierre Courtieu | |
| 2015-10-09 | Fixing 4096 character limit of scomint-send-input. | Pierre Courtieu | |
| Extended the fix of #453 (trac tracker) for emacs 25 (>=24 instead of = 24). | |||
| 2015-10-09 | Fixing < 25 use of window-frame (mandatory arg). | Pierre Courtieu | |
| 2015-10-06 | Put 'delete-selection t on coq-terminator-insert | Clément Pit--Claudel | |
| delete-selection-mode requires command that insert text to be annotated with a 'delete-selection property. | |||
| 2015-10-06 | Move .cvsignore to .gitignore | Clément Pit--Claudel | |
| 2015-10-06 | Trying to deal with debug mode. | Pierre Courtieu | |
| 2015-09-29 | colorizing hypothesis in compact mode. | Pierre Courtieu | |
| 2015-09-29 | Fixed #1 (Missing space in coq-insert-intros). | Pierre Courtieu | |
| Added a newline and removed the useless intros. | |||
| 2015-09-29 | Cleaned TODO file in coq/. | Pierre Courtieu | |
| 2015-09-25 | More Fixes when issuing commands from another buffer. | Pierre Courtieu | |
| 2015-09-25 | Fixed bug when issuing commands from another buffer than scripting one. | Pierre Courtieu | |
| Hooks modifying things in *goals* or *response* now try to operate on the right frame/windows. | |||
| 2015-09-22 | hyps highlighting now supports compact contexts (in coq trunk soon). | Pierre Courtieu | |
| 2015-06-23 | Added a moderate support for double quotes in -arg lines of _CoqProject. | Pierre Courtieu | |
| 2015-06-23 | Update to CHANGE. | Pierre Courtieu | |
| 2015-05-19 | robustify last commit (disabling smie show-paren). | Pierre Courtieu | |
| 2015-05-19 | Disable smie parenthesis blink. Too slow sometimes. | Pierre Courtieu | |
| 2015-05-07 | Fixes #492. fixed regexp (\\< --> \\_< everywhere). | Pierre Courtieu | |
| Surprising that this did not raise before... | |||
| 2015-05-07 | Fixes #484. Added syntax. | Pierre Courtieu | |
| 2015-05-07 | Fixes #485. | Pierre Courtieu | |
| 2015-05-07 | Fixes #486 with an option. | Pierre Courtieu | |
| 2015-05-07 | Yet another half fix of smie lexer. | Pierre Courtieu | |
| || is either a boolean operator or a tactical. | |||
| 2015-04-27 | Fixed at-point detection (bis). | Pierre Courtieu | |
| 2015-04-27 | Fixed at-point detection. | Pierre Courtieu | |
| 2015-04-14 | bold unicode biders + Fixing highlighting in goals and response buffers + ↵ | Pierre Courtieu | |
| cleaning. | |||
| 2015-04-13 | Debugging font-lock for ∀, ∃, and λ. | Pierre Courtieu | |
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |