aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2016-01-24basic proof tree changes for Coq 8.5Hendrik Tews
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
2016-01-19Cleaning CHANGES.Pierre Courtieu
2016-01-19fix #36.Pierre Courtieu
2016-01-14Add a few comments to explain values of coq-load-pathClément Pit--Claudel
2016-01-14Mark coq-load-path-include-current as obsoleteClément Pit--Claudel
2016-01-14Automatically detect which version of Coq we're usingClément Pit--Claudel
2016-01-14Refactor the project file parsing codeClément Pit--Claudel
2016-01-14Fix #29 + indentation glitch + regexp refactoring.Pierre Courtieu
2016-01-08Fixing indentation of ";".Pierre Courtieu
Local/Global Tactic Notation
2016-01-08indentation of ";" more accurate.Pierre Courtieu
Now detecting if the ; is inside a parenthesized tactic (--> no spurious indentation).
2016-01-08Fixing outdenting in ";" indetation.Pierre Courtieu
2016-01-08Trying to indent ";" differently inside Ltac defs.Pierre Courtieu
This only works when the command starts with "Ltac". Ideally we would like to switch to no indentation of ";" each time the ";" is the child of something else that ends a command "." or bullets).
2016-01-07Fixed indentation of ";" tactical.Pierre Courtieu
2016-01-06Merge pull request #22 from ProofGeneral/fix-scrolling-buffersPierre Courtieu
Fix spurious scrolling of *goals* and *response* buffers
2016-01-06updating CHANGESPierre Courtieu
2016-01-06Adding uset preference coq-indent-semicolon-tactical.Pierre Courtieu
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.
2016-01-06Fixing #25.Pierre Courtieu
proof-script-buffer was not set before calling proof-shell-ready-prover.
2016-01-06Fixing #20. #19 fixed by a commit in coq-8.5.Pierre Courtieu
2016-01-04First try to fix #19 and #20. Not finished.Pierre Courtieu
Maybe need coq fix.
2015-12-31Fix spurious scrolling of *goals* and *response* buffersClément Pit--Claudel
See https://github.com/cpitclaudel/company-coq/issues/8 and https://github.com/cpitclaudel/company-coq/issues/32 for some background info.
2015-12-31comment and readme.Pierre Courtieu
2015-12-14Refactoring. New file coq-system.el.Pierre Courtieu
2015-12-14Small refactoring of coqxxx args detection.Pierre Courtieu
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.
2015-12-14Fixing coq-prog-arg for auto compilation.Pierre Courtieu
2015-12-10Fixing variable declaration.Pierre Courtieu
2015-12-09Adding an setting for Search Blacklist coq option.Pierre Courtieu
2015-12-07Speeding up indentation (regexp optim).Pierre Courtieu
2015-12-07Speeding up indentation.Pierre Courtieu
Dedicated regexp for bullets when searching backward.
2015-12-05Fixed #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-04Fixed a typo.Pierre Courtieu
2015-11-30Speeding up indentation code (smie lexer).Pierre Courtieu
2015-11-30Updated the CHANGES files, mainly git url.Pierre Courtieu
2015-11-26A 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-23Introduce a coq-question-mark-faceClément Pit--Claudel
Closes #12
2015-11-17recompilation: Improve error checkingClé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-13compilation fix (coq-pre-v85).Pierre Courtieu
2015-11-13Experimenting less brutal frame deletion.Pierre Courtieu
Only in coq mode for now. There are still some strange frame deletion some times.
2015-11-13Fixed auto-width setting not initialized (trac #456).Pierre Courtieu
2015-11-13Cleaning code for auto width adapting.Pierre Courtieu
Less guessing, separate guessing code.
2015-11-12Tentative fix for #10Clément Pit--Claudel
2015-11-12Close #9Clément Pit--Claudel
2015-11-12Debuging: 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-02coq-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-20Re-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-15Fixed the regexp for colorizing hyps in the goal.Pierre Courtieu
2015-10-13Fixed coq-id-at-point.Pierre Courtieu
2015-10-13proof-retract-command-hook added + more auto adjust width in coq mode.Pierre Courtieu
2015-10-12proof-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-09Trying to not delete frames too eagerly when laying out.Pierre Courtieu
2015-10-09Fixing 4096 character limit of scomint-send-input.Pierre Courtieu
Extended the fix of #453 (trac tracker) for emacs 25 (>=24 instead of = 24).
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 01:11:05 +0000