| Age | Commit message (Collapse) | Author |
|---|
|
It needs more tweaking when a bloc is asserted at once.
|
|
|
|
When "Suggest Proof Using" is set in coq, coq suggests "Proof using"
annotations. We insert these annotation (by default after asking the
user).
|
|
Note that currently, there is no keybinding associated to the electric
terminator.
|
|
Fix documentation about Coq electric terminator
Related: #160
|
|
|
|
Add support for core Ltac2 syntax
|
|
- Ltac2 definitions, types, and notation
- Ltac2 queries
- ltac1:(...) and ltac2:(...) antiquotations
Closes #473.
|
|
|
|
|
|
|
|
For the record:
- "-topfile" option is good so that coqtop understands the name of the
current module
- but some people want to script coq files with incorrect names
without ever comiling them. So we don't add "-topfile" option when it
would make coqtop fail. A warning is issued.
|
|
|
|
|
|
|
|
Namely monadic notations and Equations (the latter is bugged
currently).
|
|
Fixed making the lexer detect the number after "do".
|
|
faces: Extend highlights to EOL to adjust for latest Emacs changes
|
|
|
|
Generic monadic indentation + specifically ext-lib / Compcert + doc.
|
|
This a generalization of PR#451 proposed by @Chobbes.
Since these syntax are not completely universal (and not builtin in
coq), the idea is to make the syntax customizable, especially to make
it possible to disable it.
NOTE: to make the Compcert syntax supported I had to refine the smie
lexer so that the ";" token was emitted as a fllback instead of ";
tactic".
NOTE2: I had to make the coq-user-token and coq-monadic-tokens be
tested ON THE RESULT of smie-coq-backward-token.
|
|
|
|
Recognize "Timeout" before save keywords to fix #446
|
|
viz. '("Defined" "Save" "Qed" "End" "Admitted" "Abort" "Proof")
|
|
Uncommented coq-find-comment-start, coq-find-comment-end as quick fix for #444
|
|
|
|
Make -topfile facility work for unnamed files
|
|
|
|
coq-par-compile: fix 8.10 -schedule-vio2vo incompatibility
|
|
Use coqc for vio2vo compilation instead of coqtop for
Coq >= 8.10+alpha.
With https://github.com/coq/coq/pull/8690 vio2vo
compilation (-schedule-vio2vo) was moved from coqtop to coqc, see
also https://github.com/coq/coq/issues/10679. This commit makes
PG compilation compatible with Coq after that PR. However, the
patch only checks for the Coq version, therefore making PG vio2vo
compilation fail on 8.10 versions before PR 8690. (Compilation
still works, it's just that vio2vo postprocessing for the mode
quick-and-vio2vo fails.)
|
|
Backtrack -> BackTo
|
|
|
|
Coq script example to reproduce:
--8<---------------cut here---------------start------------->8---
Set Nested Proofs Allowed.
Lemma foo : True /\ 1 = 1.
split. (*2*)
easy.
Goal True /\ 2 = 2. (*1-bug*)
Proof. (*1-ok*)
split; easy.
Qed.
easy.
Qed.
--8<---------------cut here---------------end--------------->8---
1. goto-point (*1-bug*) (just before the comment)
2. goto-point (*2*) (bug: the goal is not shown)
3. goto-point (*1-ok*) (just after "Proof.")
4. goto-point (*2*) (no bug)
|
|
href: coq/coq#10574
* Define a variable coq--retract-naborts to handle the communication
of [coq-find-and-forget -> coq-empty-action-list-command] that used
to be done through the third argument of Backtrack.
* Refactor coq-empty-action-list-command, replacing the occurrences of
string-match with string-match-p.
|
|
fix coqtags that can't find some theorem and output empty definition
|
|
|
|
Due to performance issue (probably an emacs bug) and given the
uselessness of the pghelp spans in retracted regions. We simply remove
these spans when retracting.
The question remains to remove them completely or to make them more
useful. company-coq currently disables them anyway.
|
|
|
|
Proof diffs revisions requested by @monnier
|
|
|
|
|
|
Remove stray h
|
|
Fixes #424
|
|
(coq-insert-with-face): Don't assume we're at EOB.
* generic/pg-goals.el (pg-goals-display): Use with-current-buffer.
* generic/pg-response.el (pg-response-maybe-erase): Narrow the scope of
inhibit-read-only.
(pg-response-display-with-face): Use `member`. Remove unused var `end`.
Only bind `start` when we have a value for it.
(proof-trace-buffer-display): Use with-current-buffer.
|
|
Support Coq's proof diffs feature: highlight diffs in goals and some error messages
|
|
FIX #422.
|
|
the output of coqtop-help is now stored in a variable like coq's version.
|
|
context (with diff annotations when enabled).
|
|
This bug seems to date from the generalization performed in commit:
080babbb0f361885e9b502ee56dec14351104a37
|
|
This patch allows one to load the `coq-diffs' option at Coq startup,
provided the ambient Coq version is >= 8.10.
This additional "lambda" format is needed because [Set Diffs "on".] is neither:
- a boolean setting from Coq side (there are three possible values)
- a string setting from Emacs side (it is implemented as a radio/symbol option)
- a cross-version compatible Coq setting.
|
