Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | fix :get for coq-search-blacklist | Hendrik Tews | 2016-12-15 | |
| | ||||
* | Merge pull request #101 from tchajed/print-universes-option | hendriktews | 2016-12-15 | |
|\ | | | | | Add Set Printing Universes to options menu | |||
* | | fix customize-group coq | Hendrik Tews | 2016-11-30 | |
| | | ||||
| * | Add Set Printing Universes to options menu | Tej Chajed | 2016-08-15 | |
|/ | ||||
* | Replace "Set Implicit Arguments" option with "Set Printing Implicit". | Erik Martin-Dorel | 2016-08-14 | |
| | | | | Closes #99. | |||
* | Coq: option to prefer top over bottom of concl. | Pierre Courtieu | 2016-06-23 | |
| | ||||
* | Merge branch 'master' of github.com:ProofGeneral/PG | Pierre Courtieu | 2016-05-20 | |
|\ | ||||
* | | Fix #72+ make user keywords prioritized over default ones. | Pierre Courtieu | 2016-05-20 | |
| | | ||||
| * | Merge branch 'master' of github.com:ProofGeneral/PG | Clément Pit--Claudel | 2016-05-16 | |
| |\ | |/ |/| | ||||
| * | Don't offer "" as the default in C-c C-c C-a | Clément Pit--Claudel | 2016-05-16 | |
| | | ||||
* | | Merge branch 'master' of github.com:ProofGeneral/PG | Pierre Courtieu | 2016-05-02 | |
|\| | ||||
* | | Fixing detection of symbol at point. | Pierre Courtieu | 2016-05-02 | |
| | | | | | | | | | | | | Quote at start of a word should not be considered part of the word. Other characters than ' or _ are punctuation. | |||
| * | Don't use string-empty-p | Clément Pit--Claudel | 2016-04-25 | |
| | | | | | | | | It's too recent | |||
| * | Respect user settings in coq-insert-intros | Clément Pit--Claudel | 2016-04-14 | |
|/ | | | | Fixes #67. | |||
* | Option to toggle optimising response windo heigth. | Pierre Courtieu | 2016-03-21 | |
| | ||||
* | Fixed #64 again. e2c5da0 commits was wrong. | Pierre Courtieu | 2016-03-09 | |
| | ||||
* | Fix #64. Use syntax-ppss in fill-nobreak-predicate. | Pierre Courtieu | 2016-03-09 | |
| | | | | | More robust to font-lock tweaks that change font inside comments (whitespace mode etc). | |||
* | Fixing #62. | Pierre Courtieu | 2016-03-08 | |
| | | | | | I don't know if it is a coq bug that bullet do not support Time. I remove Time from bullets for the moment. | |||
* | Redo 11b03d4 (ensure that ‘Time’ isn't added to internal commands) | Clément Pit--Claudel | 2016-02-29 | |
| | ||||
* | Don't add the ‘Time’ prefix to internal Coq commands | Clément Pit--Claudel | 2016-02-28 | |
| | | | | | This ensures that parts of Proof General that use Coq commands in the background are not confused by extra timing information. | |||
* | Merge pull request #40 from hendriktews/proof-tree | Pierre Courtieu | 2016-02-17 | |
|\ | | | | | basic proof tree changes for Coq 8.5 | |||
* | | Fixed recent coq syntax change (tac !H become tac (H)). | Pierre Courtieu | 2016-01-27 | |
| | | ||||
| * | basic proof tree changes for Coq 8.5 | Hendrik Tews | 2016-01-24 | |
|/ | | | | | | Fixes to get basic proof tree functionality, including support for give_up, cycle, swap, revgoals. Unshelve and evar's don't work yet, see proof-tree issues #1 and #2 | |||
* | Merge pull request #22 from ProofGeneral/fix-scrolling-buffers | Pierre Courtieu | 2016-01-06 | |
|\ | | | | | Fix spurious scrolling of *goals* and *response* buffers | |||
* | | Fixing #25. | Pierre Courtieu | 2016-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. | Pierre Courtieu | 2016-01-06 | |
| | | ||||
* | | First try to fix #19 and #20. Not finished. | Pierre Courtieu | 2016-01-04 | |
| | | | | | | | | Maybe need coq fix. | |||
| * | Fix spurious scrolling of *goals* and *response* buffers | Clément Pit--Claudel | 2015-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. | Pierre Courtieu | 2015-12-31 | |
| | | ||||
* | | Refactoring. New file coq-system.el. | Pierre Courtieu | 2015-12-14 | |
|/ | ||||
* | Small refactoring of coqxxx args detection. | Pierre Courtieu | 2015-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 variable declaration. | Pierre Courtieu | 2015-12-10 | |
| | ||||
* | Adding an setting for Search Blacklist coq option. | Pierre Courtieu | 2015-12-09 | |
| | ||||
* | Fixed a typo. | Pierre Courtieu | 2015-12-04 | |
| | ||||
* | A shortcut for coq-insert-as-in-next-command. | Pierre Courtieu | 2015-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). | |||
* | Experimenting less brutal frame deletion. | Pierre Courtieu | 2015-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). | Pierre Courtieu | 2015-11-13 | |
| | ||||
* | Cleaning code for auto width adapting. | Pierre Courtieu | 2015-11-13 | |
| | | | | Less guessing, separate guessing code. | |||
* | Tentative fix for #10 | Clément Pit--Claudel | 2015-11-12 | |
| | ||||
* | Debuging: display a warning. | Pierre Courtieu | 2015-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]. | Pierre Courtieu | 2015-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. | Pierre Courtieu | 2015-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 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-13 | |
| | ||||
* | proof-assert-command-hook added + Auto adjust width in coq mode. | Pierre Courtieu | 2015-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). | Pierre Courtieu | 2015-10-09 | |
| | ||||
* | Put 'delete-selection t on coq-terminator-insert | Clément Pit--Claudel | 2015-10-06 | |
| | | | | | delete-selection-mode requires command that insert text to be annotated with a 'delete-selection property. | |||
* | Trying to deal with debug mode. | Pierre Courtieu | 2015-10-06 | |
| | ||||
* | Fixed #1 (Missing space in coq-insert-intros). | Pierre Courtieu | 2015-09-29 | |
| | | | | Added a newline and removed the useless intros. | |||
* | More Fixes when issuing commands from another buffer. | Pierre Courtieu | 2015-09-25 | |
| |