aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-10-16Fix #514 + support for named goal selector.Pierre Courtieu
It was hard to separate this too fixes (same regexps).
2020-10-16Fix #518: "Proof using" mode corrupts "Proof with tac".Pierre Courtieu
2020-10-14Merge pull request #517 from Lysxia/hl-computeClément Pit-Claudel
Highlight Compute
2020-10-14Highlight ComputeLi-yao Xia
2020-09-11fix(coq/coq.el): spelling of "whether" (#512)dymil
2020-09-11fix(CHANGES): spelling of "whether" (#511)dymil
2020-09-11Update PhoX link and add https (#510)dymil
2020-06-23Merge pull request #503 from hendriktews/issue-499-ancestor-appendErik Martin-Dorel
coq-par-compile: use hash for ancestors
2020-06-20Merge pull request #501 from haselwarter/proof-shell-string-match-safeErik Martin-Dorel
Use `proof-shell-string-match-safe` to avoid failing on `nil` regexp
2020-06-19coq-par-compile: use hash for ancestorsHendrik Tews
The hash avoids an exponentially growing number of duplicates in the ancestor collection. Fixes #499
2020-06-18Use `proof-shell-string-match-safe` to avoid failing on `nil` regexpPhilipp G. Haselwarter
Fixes a regression introduced in 22681a3caf2c8f45700585ea74dffbf48bb2ac19. In particular, the Coq module seems to be the only one currently setting `proof-show-proof-diffs-regexp`, causing an error for EasyCrypt.
2020-06-15Add coloration for Ltac2 commandsCyril Anaclet
Close #489
2020-06-04New hook for early prompt/output analyzis.Pierre Courtieu
proof-state-change-pre-hook happens earlier than proof-state-change-hook, i.e. before proof-done-advancing. This should be used to register information in the currently processed span before proof-done-advancing classifies it. Historically PG design was to gather these information during proof-done-advancing (or in its hook called at the end) by just looking at the command statement. But it is often useful to look at the output (messages and/or prompt) to gather more accurate information. Some of this information may be needed DURING proof-done-advancing. Hence this early hook.
2020-05-29Merge pull request #490 from ProofGeneral/feature/487Erik Martin-Dorel
Improve PG support of Show Proof (Diffs): Display the proof terms stepwise in the *response* buffer. Close #487
2020-05-29refactor: Remove unneeded coq-should-responseErik Martin-Dorel
2020-05-29Minor changesAnaclet
2020-05-29Fix the test 081Anaclet
2020-05-29Add tests and flags systemAnaclet
2020-05-29fix: backtrack for "Show Proof" disabledAnaclet
2020-05-29fix: backtrack wrong type argumentAnaclet
2020-05-29fix: Do "Show Proof…" (with "?Goal") as soon as the proof is startedErik Martin-Dorel
2020-05-29test: Add regression test (currently failing)Erik Martin-Dorel
2020-05-29Apply reviews of @erikmdCyril Anaclet
2020-05-29WIP for #487Cyril Anaclet
2020-05-29Fix name clash & rephrase some stringsErik Martin-Dorel
2020-05-29All case for Show and regex variableCyril Anaclet
2020-05-29First try for feature #487Cyril Anaclet
2020-05-28Merge pull request #496Erik Martin-Dorel
fix: test files should not provide features Fix #493 further
2020-05-28Added a few coq commands.Pierre Courtieu
2020-05-28fix: test files should not provide featuresErik Martin-Dorel
href: https://github.com/ProofGeneral/PG/issues/493#issuecomment-634493988
2020-05-28Fix default value for proof-shell-last-cmd-left-goals-p.Pierre Courtieu
This variable was still not used anywhere, but will soon.
2020-05-27Add proof-shell-last-cmd-left-goals-p.Pierre Courtieu
Prover specific analyzis of the last prompt/output to determine if there are open goals left.
2020-05-26[CI] Also run integration tests with Coq 8.9.1 and 8.10.2Erik Martin-Dorel
href: https://github.com/coq-community/docker-coq/wiki#supported-tags
2020-05-26fix: test files should not provide featuresErik Martin-Dorel
Close #493
2020-05-06Merge pull request #488 from Flupp/doc-info-menu-fixErik Martin-Dorel
doc/ProofGeneral.texi: fix makeinfo
2020-05-06test: Add CI step to build the docErik Martin-Dorel
* Only build the info manual. * Otherwise we would get the following issue: $ texi2pdf PG-adapting.texi You don't have a working TeX binary (tex) installed anywhere in your PATH, and texi2dvi cannot proceed without one. If you want to use this script, you'll need to install TeX (if you don't have it) or change your PATH or TEX environment variable (if you do). See the --help output for more details. For information about obtaining TeX, please see http://tug.org/texlive, Makefile.doc:50: recipe for target 'PG-adapting.pdf' failed or do a web search for TeX and your operating system or distro. On Debian you can install a working TeX system with apt-get install texlive
2020-05-06doc/ProofGeneral.texi: fix makeinfoToni Dietze
Fixes the following error: node `Coq Proof General' lacks menu item for `Proof using annotations' despite being its Up target
2020-05-04Merge pull request #486 from ProofGeneral/coq-tests-for-masterErik Martin-Dorel
Coq tests for master
2020-05-04docs: Add a comment in ci/test_wholefile.vErik Martin-Dorel
* see also https://github.com/ProofGeneral/PG/issues/485
2020-05-04add testCyril Anaclet
2020-05-04Fixing #485, bug on proof without "Proof".Pierre Courtieu
Due to a re-search that should fail silently.
2020-05-04refactor: Rename test fileErik Martin-Dorel
2020-05-04test: Remove "Proof." workaroundErik Martin-Dorel
2020-05-04docs: Add docstrings in testsErik Martin-Dorel
2020-05-04Fixing #485, bug on proof without "Proof".Pierre Courtieu
Due to a re-search that should fail silently.
2020-05-04refactor: Remove unneeded auxiliary functions & Use "coq-" prefixErik Martin-Dorel
2020-05-04fix: ert.jsonErik Martin-Dorel
* The zone between "Test ... condition:" & "FAILED ..." can have more than 1 line!
2020-05-04fix: Tweak comments and workaround ProofGeneral/PG#485Erik Martin-Dorel
2020-05-04test: Add tests and some fixCyril Anaclet
2020-05-01fix: add some "sudo chown coq:coq" commandErik Martin-Dorel
* This should solve the "(buffer-read-only #<buffer test1.v>)" error, probably due to permission issues.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 07:07:58 +0000