aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-04-21fix: Install emacs in the Docker containerErik Martin-Dorel
2020-04-17feat: Update test.yml to trigger integration testsErik Martin-Dorel
* Fix test.sh so it can be run from the parent dir
2020-04-17feat: Add first version of coq-tests.elErik Martin-Dorel
TODO: Expand it using - https://github.com/rejeep/ert-async.el - and/or https://www.gnu.org/software/emacs/manual/html_node/ert/index.html
2020-04-17chore: Add shell script to automate the testsErik Martin-Dorel
* Inspired by https://github.com/pfitaxel/learn-ocaml.el/blob/master/test.sh (under license MIT)
2020-04-16chore: Add init-tests.elErik Martin-Dorel
* Taken from https://github.com/pfitaxel/learn-ocaml.el/blob/master/tests/init-tests.el (under license MIT)
2020-04-16feat: Add GitHub-action workflowErik Martin-Dorel
2020-04-16feat: Remove Travis CI configurationErik Martin-Dorel
2020-04-10docs: Update CHANGES after issue #479 and PR #480Erik Martin-Dorel
* Make (coq-insert-intros) conditionnaly insert `move=>` or `intros`
2020-04-10Merge branch 'master' of https://github.com/ProofGeneral/PGPierre Courtieu
2020-04-10Fixed proof using annotation mechanism.Pierre Courtieu
I ended up using (in a slight devious way) the lemma dependency mechanism of PG: the dependency information stored in the span is only the ones suggested by coq: only the one that should appear in theproof using annotation (and only when coq felt the need to suggest them.
2020-04-10Merge pull request #480 from CyrilAnac/masterErik Martin-Dorel
feat(coq-insert-intros): Conditionally insert `move=>` or `intros`
2020-04-10Close #479cyrilzak31
2020-04-09Unplugging previous commit (proof using insertion.Pierre Courtieu
It needs more tweaking when a bloc is asserted at once.
2020-04-09Merge branch 'master' of https://github.com/ProofGeneral/PGPierre Courtieu
2020-04-09Automatic "Proof using" insertion.Pierre Courtieu
When "Suggest Proof Using" is set in coq, coq suggests "Proof using" annotations. We insert these annotation (by default after asking the user).
2020-04-02Rephrase ProofGeneral.texi following PR #476 that fixed #475Erik Martin-Dorel
Note that currently, there is no keybinding associated to the electric terminator.
2020-04-02Merge pull request #476 from dunnl/issue-475Erik Martin-Dorel
Fix documentation about Coq electric terminator Related: #160
2020-04-02Correct documentationLawrence Dunn
2020-04-02Merge pull request #474 from tchajed/add-ltac2-syntaxErik Martin-Dorel
Add support for core Ltac2 syntax
2020-04-02Add support for core Ltac2 syntaxTej Chajed
- Ltac2 definitions, types, and notation - Ltac2 queries - ltac1:(...) and ltac2:(...) antiquotations Closes #473.
2020-04-01SearchAbout is deprecated since 8.5; use Search insteadClément Pit-Claudel
2020-04-01Change "" into nil in argument to appendClément Pit-Claudel
2020-03-26Cleaning previous commit, following @cpitclaudel advices.Pierre Courtieu
2020-03-26Fix #472. Removed -topfile when file name incorrect.Pierre Courtieu
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.
2020-03-13Fix 464: proof-autoloads not found by EmacsPierre Courtieu
2020-03-12moving tests for monadic notations and Equations in separate files.Pierre Courtieu
2020-03-12Fix #465: Indentation of Equations (plugin).Pierre Courtieu
2020-03-02Adding Tests for indentation related to plugins.Pierre Courtieu
Namely monadic notations and Equations (the latter is bugged currently).
2020-03-02Fix #462.Pierre Courtieu
Fixed making the lexer detect the number after "do".
2020-02-06Merge pull request #455 from ProofGeneral/cpitclaudel_extend_facesClément Pit-Claudel
faces: Extend highlights to EOL to adjust for latest Emacs changes
2020-01-31faces: Extend highlights to EOL to adjust for latest Emacs changesClément Pit-Claudel
2020-01-20Merge pull request #452 from Matafou/fix_monadicPierre Courtieu
Generic monadic indentation + specifically ext-lib / Compcert + doc.
2020-01-19Generic monadic indentation + specifically ext-lib / Compcert + doc.Pierre Courtieu
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.
2020-01-13Fixing /\ and \/ priority for indentation purpose.Pierre Courtieu
2019-12-09Merge pull request #447 from ProofGeneral/fix-gh-446Erik Martin-Dorel
Recognize "Timeout" before save keywords to fix #446
2019-12-08fix: Recognize "Timeout" before save keywordsErik Martin-Dorel
viz. '("Defined" "Save" "Qed" "End" "Admitted" "Abort" "Proof")
2019-12-05Merge pull request #445 from vzaliva/patch-1Erik Martin-Dorel
Uncommented coq-find-comment-start, coq-find-comment-end as quick fix for #444
2019-12-04Uncommented coq-find-comment-start, coq-find-comment-end as quick fix for #444Vadim Zaliva
2019-10-07Merge pull request #443 from pi8027/topfile-unnamedErik Martin-Dorel
Make -topfile facility work for unnamed files
2019-10-07Make -topfile facility work for unnamed filesKazuhiko Sakaguchi
2019-08-21Merge pull request #438 from hendriktews/fix-vio2vo-8-10Erik Martin-Dorel
coq-par-compile: fix 8.10 -schedule-vio2vo incompatibility
2019-08-21coq-par-compile: fix 8.10 -schedule-vio2vo incompatibilityHendrik Tews
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.)
2019-07-27Merge pull request #434 from gares/patch-1Clément Pit-Claudel
Backtrack -> BackTo
2019-07-26fix: Add missing "Set Diffs ..." command in some backtracking caseErik Martin-Dorel
2019-07-26fix: corner case where "Show." was not triggered.Erik Martin-Dorel
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)
2019-07-26Backtrack -> BackToEnrico Tassi
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.
2019-07-25Merge pull request #432 from a0919610611/fix-coqtagsPierre Courtieu
fix coqtags that can't find some theorem and output empty definition
2019-07-25fix coqtags that can't find some theorem and output empty definition nameYu-Fu Fu
2019-06-18Remove pghelp spans when retracting.Pierre Courtieu
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.
2019-06-17fixing with inductive indentation.Pierre Courtieu
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 12:48:53 +0000