| Commit message (Collapse) | Author | Age |
| |
|
|\ |
|
| | |
|
| |\
| |/
|/| |
|
| | |
|
|\| |
|
| |
| |
| |
| |
| |
| | |
Quote at start of a word should not be considered part of the word.
Other characters than ' or _ are punctuation.
|
| |
| |
| |
| | |
It's too recent
|
|/
|
|
| |
Fixes #67.
|
| |
|
| |
|
|
|
|
|
| |
More robust to font-lock tweaks that change font inside
comments (whitespace mode etc).
|
|
|
|
|
| |
I don't know if it is a coq bug that bullet do not support Time. I
remove Time from bullets for the moment.
|
| |
|
|
|
|
|
| |
This ensures that parts of Proof General that use Coq commands in the
background are not confused by extra timing information.
|
|\
| |
| | |
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
|
|\
| |
| | |
Fix spurious scrolling of *goals* and *response* buffers
|
| |
| |
| |
| | |
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.
|
| |
|
| |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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).
|
|
|
|
|
| |
Only in coq mode for now. There are still some strange frame deletion
some times.
|
| |
|
|
|
|
| |
Less guessing, separate guessing code.
|
| |
|
|
|
|
|
| |
The warning is displayed when failing to retrieve last prompt info. Once
we understand what happened we can remove this warning.
|
|
|
|
|
|
| |
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.
|
|
|
|
|
|
|
|
|
| |
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.
|
| |
|
| |
|
|
|
|
|
|
|
| |
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).
|
| |
|
|
|
|
|
| |
delete-selection-mode requires command that insert text to be annotated
with a 'delete-selection property.
|
| |
|
|
|
|
| |
Added a newline and removed the useless intros.
|
| |
|
|
|
|
|
| |
Hooks modifying things in *goals* or *response* now try to operate on
the right frame/windows.
|
| |
|
| |
|
| |
|
| |
|