| Age | Commit message (Collapse) | Author |
|---|
|
if a "; tactic" is not at the end of its line, (hanging) then it should
not act on indetation of next line.
|
|
|
|
I don't know if it is a coq bug that bullet do not support Time. I
remove Time from bullets for the moment.
|
|
|
|
|
|
|
|
Also refactor coq-font-lock-keywords-1 slightly.
|
|
|
|
|
|
This ensures that parts of Proof General that use Coq commands in the
background are not confused by extra timing information.
|
|
|
|
|
|
This is useful if people want to set them project-locally.
|
|
|
|
basic proof tree changes for Coq 8.5
|
|
|
|
|
|
|
|
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
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Local/Global
Tactic Notation
|
|
Now detecting if the ; is inside a parenthesized tactic (--> no spurious
indentation).
|
|
|
|
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).
|
|
|
|
Fix spurious scrolling of *goals* and *response* buffers
|
|
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.
|
|
proof-script-buffer was not set before calling proof-shell-ready-prover.
|
|
|
|
Maybe need coq fix.
|
|
See https://github.com/cpitclaudel/company-coq/issues/8 and
https://github.com/cpitclaudel/company-coq/issues/32 for some background
info.
|
|
|
|
|
|
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.
|
|
|
|
|
|
|
|
|
|
Dedicated regexp for bullets when searching backward.
|
|
Experimenting on more regexp and less adhoc searching in the smie lexer.
In particular the regexp for bullet seems now capture only real bullets.
|
|
|
|
|
|
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).
|
|
Closes #12
|
|
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)
|
