aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq
Commit message (Collapse)AuthorAge
...
* Merge pull request #22 from ProofGeneral/fix-scrolling-buffersGravatar Pierre Courtieu2016-01-06
|\ | | | | Fix spurious scrolling of *goals* and *response* buffers
* | Adding uset preference coq-indent-semicolon-tactical.Gravatar Pierre Courtieu2016-01-06
| | | | | | | | | | | | | | | | | | Some people prefer ";" tactical to be non indented, in particular in Ltac definitions. Setting this variable to 0 (2 by default) does it. You can still have some indentation by putting ; at beginning of lines: tac1 ; tac2 ; tac3.
* | Fixing #25.Gravatar Pierre Courtieu2016-01-06
| | | | | | | | proof-script-buffer was not set before calling proof-shell-ready-prover.
* | Fixing #20. #19 fixed by a commit in coq-8.5.Gravatar Pierre Courtieu2016-01-06
| |
* | First try to fix #19 and #20. Not finished.Gravatar Pierre Courtieu2016-01-04
| | | | | | | | Maybe need coq fix.
| * Fix spurious scrolling of *goals* and *response* buffersGravatar Clément Pit--Claudel2015-12-31
| | | | | | | | | | | | See https://github.com/cpitclaudel/company-coq/issues/8 and https://github.com/cpitclaudel/company-coq/issues/32 for some background info.
* | comment and readme.Gravatar Pierre Courtieu2015-12-31
| |
* | Refactoring. New file coq-system.el.Gravatar Pierre Courtieu2015-12-14
|/
* Small refactoring of coqxxx args detection.Gravatar Pierre Courtieu2015-12-14
| | | | | | Need some more refactoring actually: Some code from coq-compile-common became necessary to coq/pg globally. We shoudl refelct this by moving these parts somewhere else.
* Fixing coq-prog-arg for auto compilation.Gravatar Pierre Courtieu2015-12-14
|
* Fixing variable declaration.Gravatar Pierre Courtieu2015-12-10
|
* Adding an setting for Search Blacklist coq option.Gravatar Pierre Courtieu2015-12-09
|
* Speeding up indentation (regexp optim).Gravatar Pierre Courtieu2015-12-07
|
* Speeding up indentation.Gravatar Pierre Courtieu2015-12-07
| | | | Dedicated regexp for bullets when searching backward.
* Fixed #15 + more speedup of indentation.Gravatar Pierre Courtieu2015-12-05
| | | | | Experimenting on more regexp and less adhoc searching in the smie lexer. In particular the regexp for bullet seems now capture only real bullets.
* Fixed a typo.Gravatar Pierre Courtieu2015-12-04
|
* Speeding up indentation code (smie lexer).Gravatar Pierre Courtieu2015-11-30
|
* A shortcut for coq-insert-as-in-next-command.Gravatar Pierre Courtieu2015-11-26
| | | | | | | | | | | | | 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).
* Introduce a coq-question-mark-faceGravatar Clément Pit--Claudel2015-11-23
| | | | Closes #12
* recompilation: Improve error checkingGravatar Clément Pit--Claudel2015-11-17
| | | | | | | | | | | | | | | | | | | | | | | | | 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)
* compilation fix (coq-pre-v85).Gravatar Pierre Courtieu2015-11-13
|
* Experimenting less brutal frame deletion.Gravatar Pierre Courtieu2015-11-13
| | | | | Only in coq mode for now. There are still some strange frame deletion some times.
* Fixed auto-width setting not initialized (trac #456).Gravatar Pierre Courtieu2015-11-13
|
* Cleaning code for auto width adapting.Gravatar Pierre Courtieu2015-11-13
| | | | Less guessing, separate guessing code.
* Tentative fix for #10Gravatar Clément Pit--Claudel2015-11-12
|
* Debuging: display a warning.Gravatar Pierre Courtieu2015-11-12
| | | | | The warning is displayed when failing to retrieve last prompt info. Once we understand what happened we can remove this warning.
* coq-pre-v85 option to fix coqdep invocation in [compile before require].Gravatar Pierre Courtieu2015-11-02
| | | | | | 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.
* Re-thinking auto-insert-as.Gravatar Pierre Courtieu2015-10-20
| | | | | | | | | 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.
* Fixed the regexp for colorizing hyps in the goal.Gravatar Pierre Courtieu2015-10-15
|
* Fixed coq-id-at-point.Gravatar Pierre Courtieu2015-10-13
|
* proof-retract-command-hook added + more auto adjust width in coq mode.Gravatar Pierre Courtieu2015-10-13
|
* proof-assert-command-hook added + Auto adjust width in coq mode.Gravatar Pierre Courtieu2015-10-12
| | | | | | | 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).
* Fixing < 25 use of window-frame (mandatory arg).Gravatar Pierre Courtieu2015-10-09
|
* Put 'delete-selection t on coq-terminator-insertGravatar Clément Pit--Claudel2015-10-06
| | | | | delete-selection-mode requires command that insert text to be annotated with a 'delete-selection property.
* Trying to deal with debug mode.Gravatar Pierre Courtieu2015-10-06
|
* colorizing hypothesis in compact mode.Gravatar Pierre Courtieu2015-09-29
|
* Fixed #1 (Missing space in coq-insert-intros).Gravatar Pierre Courtieu2015-09-29
| | | | Added a newline and removed the useless intros.
* Cleaned TODO file in coq/.Gravatar Pierre Courtieu2015-09-29
|
* More Fixes when issuing commands from another buffer.Gravatar Pierre Courtieu2015-09-25
|
* Fixed bug when issuing commands from another buffer than scripting one.Gravatar Pierre Courtieu2015-09-25
| | | | | Hooks modifying things in *goals* or *response* now try to operate on the right frame/windows.
* hyps highlighting now supports compact contexts (in coq trunk soon).Gravatar Pierre Courtieu2015-09-22
|
* Added a moderate support for double quotes in -arg lines of _CoqProject.Gravatar Pierre Courtieu2015-06-23
|
* robustify last commit (disabling smie show-paren).Gravatar Pierre Courtieu2015-05-19
|
* Disable smie parenthesis blink. Too slow sometimes.Gravatar Pierre Courtieu2015-05-19
|
* Fixes #492. fixed regexp (\\< --> \\_< everywhere).Gravatar Pierre Courtieu2015-05-07
| | | | Surprising that this did not raise before...
* Fixes #484. Added syntax.Gravatar Pierre Courtieu2015-05-07
|
* Fixes #485.Gravatar Pierre Courtieu2015-05-07
|
* Fixes #486 with an option.Gravatar Pierre Courtieu2015-05-07
|
* Yet another half fix of smie lexer.Gravatar Pierre Courtieu2015-05-07
| | | | || is either a boolean operator or a tactical.
* Fixed at-point detection (bis).Gravatar Pierre Courtieu2015-04-27
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 21:29:35 +0000