aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/proofs
AgeCommit message (Collapse)Author
2021-04-02Remove the omega tactic and related optionsJim Fehrle
2021-03-08Convert 2nd part of rewriting chapter to prodnJim Fehrle
2021-03-02Merge PR #13889: Dead code elimination: not reducible error message is never ↵coqbot-app[bot]
raised. Reviewed-by: jfehrle
2021-03-02Dead code elimination: not reducible error message is never raised.Théo Zimmermann
2021-02-24Infrastructure for fine-grained debug flagsMaxime Dénès
2021-01-28Update doc/sphinx/proofs/writing-proofs/rewriting.rstJim Fehrle
2021-01-28Apply suggestions from code reviewThéo Zimmermann
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2021-01-28Document how rewrite works regarding occurrence selection.Théo Zimmermann
2021-01-22Merge PR #13754: Improve doc of occurrences and rewrite.coqbot-app[bot]
Reviewed-by: Zimmi48
2021-01-22Improve doc of occurrences and rewrite.Jim Fehrle
2021-01-22Merge PR #13761: Remove convert_concl_no_check (deprecated in 8.11)Pierre-Marie Pédrot
Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2021-01-21Improve wording for #13384Jim Fehrle
2021-01-20Fix: "tactic" is not a tactic, so can't begin a .. tacn::Jim Fehrle
2021-01-19Remove convert_concl_no_checkJim Fehrle
2021-01-18Support locality attributes for Hint Rewrite (including export)Gaëtan Gilbert
We deprecate unspecified locality as was done for Hint. Close #13724
2021-01-02Deprecate "at ... with ..." in change tacticJim Fehrle
(use "with ... at ..." instead)
2021-01-01Merge PR #13470: Convert rewriting and proof-mode chapters to prodncoqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: JasonGross
2020-12-30Convert rewriting and proof-mode chapters to prodnJim Fehrle
2020-12-30Merge PR #13684: Document the -native-compiler optioncoqbot-app[bot]
Reviewed-by: silene Ack-by: Zimmi48 Ack-by: jfehrle
2020-12-29Document the -native-compiler optionPierre Roux
2020-12-21Shorten/improve intro of "Basic proof writing" chapter.Théo Zimmermann
2020-12-11doc: Clarify the status of simpl vs cbnClément Pit-Claudel
The cbn tactic was documented in aa9db490a2. The current manual causes confusion by suggesting that cbn is a replacement for simpl, while in practice they do different things, both with their own quirks. Given that neither is consistently faster than the other, I think it's worth clarifying the manual.
2020-11-27Revert "Remove deprecated tactic cutrewrite."Théo Zimmermann
This reverts commit f3642ad8bdf6d9aa1b411892e5e6815a6a75e4d5.
2020-11-24Convert auto chapter to prodnJim Fehrle
2020-11-23Merge PR #13417: Use nat_or_var in grammar where negative values don't make ↵coqbot-app[bot]
sense Reviewed-by: Zimmi48
2020-11-20Merge PR #13237: Address #13235: avoid passing degenerate in-hyps clausesPierre-Marie Pédrot
Reviewed-by: jfehrle Reviewed-by: ppedrot
2020-11-20Use nat_or_var where negative values don't make senseJim Fehrle
2020-11-18Use only nats for occs_nums rather than intsJim Fehrle
2020-11-17Fixes #13235: remove fragile tolerance for degenerate in-hyps clause.Hugo Herbelin
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
2020-11-16Merge PR #13384: Warn on hints without an explicit localitycoqbot-app[bot]
Reviewed-by: Zimmi48
2020-11-16Merge PR #12516: Deprecate `Grab Existential Variables` and `Existential` ↵Pierre-Marie Pédrot
commands Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2020-11-16Document the deprecation of the commands.Pierre-Marie Pédrot
2020-11-16Document the new warning.Pierre-Marie Pédrot
2020-11-16Tentative fix for the refman.Pierre-Marie Pédrot
2020-11-15Document the new export locality for the remaining hint commands.Pierre-Marie Pédrot
2020-11-10Convert logic.rst to prodnJim Fehrle
2020-11-09[refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina.Théo Zimmermann
The smallcaps rendering was inexistent in the PDF version and did not look good in the HTML version.
2020-11-05Improve title of first proof chapter.Théo Zimmermann
2020-11-05Change the title of the automatic tactic chapter and of its sections.Théo Zimmermann
Prefer the term 'solver' to 'decision procedure'.
2020-11-05Add new sections to automatic tactic chapter.Théo Zimmermann
2020-11-05Various fixes.Théo Zimmermann
2020-11-05Merge content from two origins into the same file.Théo Zimmermann
2020-11-05Move proof handling chapter in new location.Théo Zimmermann
2020-11-05Octopus merge to preserve history of content split over multiple files.Théo Zimmermann
2020-11-05Remove everything before goal management.Théo Zimmermann
2020-11-05Remove everything after the content on goal management.Théo Zimmermann
2020-11-05Move some content on goal management to the proof mode page.Théo Zimmermann
2020-11-05Keep only the content on solvers for logic and equality.Théo Zimmermann
2020-11-05Move some content to a new page on solvers for logic and equality.Théo Zimmermann
2020-11-05Keep only content about auto.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:57:20 +0000