aboutsummaryrefslogtreecommitdiff
path: root/coq
AgeCommit message (Collapse)Author
2021-04-21Merge pull request #559 from hendriktews/omit-proofsHEADmasterErik Martin-Dorel
Add feature to omit complete opaque proofs
2021-04-16add feature to omit complete opaque proofsHendrik Tews
This commit adds a feature to recognize complete opaque proofs in the asserted region and to replace them with an admitted proof. This can drastically improve the processing time for the asserted region at the cost of not checking the omitted proofs. Omitted proofs are displayed slightly darker compared to other parts of the locked region. With this commit, the feature is supported for Coq for files in which proofs are started with some form of Proof and ended with either Qed, Defined, Admitted or Abort. To enable, configure proof-omit-proofs-option or click Proof General -> Quick Options -> Processing -> Omit Proofs.
2021-04-08Fixing "match with" generation.Pierre Courtieu
2021-04-08Fix useless quotes generatinf warnings.Pierre Courtieu
2021-04-08Fixing hypothesis folding GUI.Pierre Courtieu
2021-03-21Fix #562. Lazy/multi_?match indentation support.Pierre Courtieu
Actually it seems that even multimatch and lazymatch was poorly supported.
2021-03-21Fix #563 avoid dual-send bug in search blacklist customization.Pierre Courtieu
Splitting the coq into two commands made me remove coq-search-blacklist-string from defpgcustom. The visible effect is that the menu entry has moved, and the command name changed. This is explained in the CHANGES. To squash.
2021-03-17coq: Update coq-prettify-symbols-alist for consistency with company-coqClément Pit-Claudel
There's no need for ("not" . ?¬) because Coq already has a "~" for it.
2021-02-22protect uses of coq-callcoqHendrik Tews
Uses of coq-callcoq need to correctly handle nil as result for the case that coq-callcoq fails. Additionally, add a regression test. Fixes #551
2021-02-13improve/fix code documentation for vok processingHendrik Tews
2021-02-13add second stage -vok for Coq >= 8.11Hendrik Tews
New value vos-and-vok for coq-compile-vos customization option, existing value vos stands now for vos-no-vok. The implementation uses the existing vio2vo infrastructure with symbols vok and vio2vo. Documentation is still missing.
2021-02-13generalize vio2vo symbol names for vok compilationHendrik Tews
In functions, variables and symbols vio2vo is replaced with second-stage to accommodate for vok compilation. For backward compatibility, the options coq-compile-vio2vo-delay and coq-max-background-vio2vo-percentage are kept. They provide default values for their renamed counterparts, if they have been set manually or through the customization system. Documentation has only been marked but not updated yet.
2021-01-31fix typos and unicode single quotations in doc stringsHendrik Tews
Backported those typos that were fixed only in the manual texi sources and not in the doc strings, from which the text was imported. Convert a few symbols quoted with curved unicode single quotations to ascii, such that make magic recognizes them.
2021-01-15Preventive support of "goal instead of "subgoal" in coq messages.Pierre Courtieu
Coq team is currently considering changing all messages containing "subgoal[s]" into "goal[s]". This commit allows for both. I make this change as early as possible, even if this chage may not land in coq's master, so that we support this as early as possible. I don't see how this could break anything but again the earliest the best.
2021-01-10add Coq compile test for a delayed requireHendrik Tews
2020-12-26make-temp-file without text argument for emacs 25Hendrik Tews
fixes #534
2020-12-19ensure vo compilation for tests, increase parallelism, more config outputHendrik Tews
2020-12-19fix 2 background compilation bugs for a dependency in state readyHendrik Tews
2020-12-19add test for recompilation with changesHendrik Tews
2020-12-19fix keep-going when dependency exists but failedHendrik Tews
2020-12-19redesign of parallel background compilation without clonesHendrik Tews
- no clones any more, existing jobs are directly linked - the whole require command is processed by coqdep to determine the required files, this fixes #352 - the require commands are a separate kind of jobs, because they do not need to get compiled - queue items are only stored in require jobs and file jobs can not have a queue dependency, this simplifies the logic
2020-12-07protect coq-callcoq against escaping signalsHendrik Tews
This hopefully fixes compilation without coqtop and especially the github tests.
2020-12-07fix coq-callcoq for emacs 27Hendrik Tews
Use process-file and omit find-file-name-handler, because process-file takes care of file handlers already. Fixes #525
2020-11-19coq: Add highlighting for Hint ModeClément Pit-Claudel
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-14Highlight ComputeLi-yao Xia
2020-09-11fix(coq/coq.el): spelling of "whether" (#512)dymil
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-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-29Minor changesAnaclet
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-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-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-04Fixing #485, bug on proof without "Proof".Pierre Courtieu
Due to a re-search that should fail silently.
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 08:08:06 +0000