aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-04-21[CI] Fix on/(push,pull_request) specErik Martin-Dorel
2020-04-21s/4.07-flambda/minimal/Erik Martin-Dorel
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-16Fix hide/show proof.Pierre Courtieu
Bug described by @MdeLv at: https://github.com/coq/coq/issues/12088#issuecomment-613266520
2020-04-15Fix a bug in detection of "Proof." when "proof using" insertionPierre Courtieu
2020-04-15Fixed disabled proof using menu.Pierre Courtieu
2020-04-15add CHANGES entry for vosHendrik Tews
2020-04-15update documentation for vos compilationHendrik Tews
2020-04-15menu entry for coq-compile-vosHendrik Tews
2020-04-15coq-par-compile: support -vos for coq >= 8.11 and default setting changeHendrik Tews
This commit adds support for the new -vos compilation. For coq >= 8.11 only -vos can be used, depending on the config option coq-compile-vos. For coq < 8.11 only -quick/-vio is used, depending on option coq-compile-quick, as before. For a smooth upgrade path, if coq-compile-vos has not been configured, the users intention on whether to use -vos or not for coq >= 8.11 is derived from coq-compile-quick. Some defaults have been changed: - parallel background compilation is the default now in case coq-compile-before-require is enabled. - for coq < 8.11, quick/vio compilation with delayed vio-to-vo conversion is now the default
2020-04-15Span menu entry for proof using annotation + doc.Pierre Courtieu
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 20:10:29 +0000