aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Collapse)Author
2021-01-26Merge PR #13758: Remove the Hide Obligations flag (deprecated in 8.12)coqbot-app[bot]
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48
2021-01-25Remove the Hide Obligations flagJim Fehrle
2021-01-24Merge PR #13762: Remove double induction tacticPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
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-21Merge PR #13764: Remove Add InjTyp and 10 other micromega commands ↵BESSON Frederic
(deprecated in 8.13) Reviewed-by: Zimmi48 Reviewed-by: fajb
2021-01-20Remove double induction tacticJim Fehrle
2021-01-20Fix: "tactic" is not a tactic, so can't begin a .. tacn::Jim Fehrle
2021-01-19Remove Add InjTyp and 10 other micromega commandsJim Fehrle
2021-01-19Remove convert_concl_no_checkJim Fehrle
2021-01-19Merge PR #13699: Fix #13579 (hnf on primitives raises an anomaly)Pierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2021-01-19Merge PR #13512: Fixes #13413: freshness failure in apply-in introduction ↵Pierre-Marie Pédrot
pattern Reviewed-by: ppedrot
2021-01-19Merge PR #13725: Support locality attributes for Hint Rewrite (including export)Pierre-Marie Pédrot
Ack-by: Zimmi48 Ack-by: gares Reviewed-by: ppedrot
2021-01-18Adding changelog for #13512.Hugo Herbelin
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-18Merge PR #13574: Simplistic patch to fix #10113: turn Ltac2's `pattern:` ↵Pierre-Marie Pédrot
into `pat:` Ack-by: Zimmi48 Reviewed-by: jfehrle Reviewed-by: ppedrot
2021-01-18Add changelogPierre Roux
2021-01-18Merge PR #13705: Improve documentation of rewrite_strat/innermost and outermostcoqbot-app[bot]
Reviewed-by: JasonGross Reviewed-by: Zimmi48 Ack-by: gares
2021-01-13Adjust the doc_grammar files.Théo Zimmermann
2021-01-07Use nat_or_var for fail/gfailJim Fehrle
2021-01-07Merge PR #13696: Deprecate "at ... with ..." in change tactic (use "with ... ↵Pierre-Marie Pédrot
at ..." instead) Ack-by: Zimmi48 Reviewed-by: ppedrot
2021-01-07Merge PR #13715: [micromega] Add missing support for `implb`Vincent Laporte
Reviewed-by: vbgl
2021-01-06Improve description of rewrite_strat/innermost and outermostJim Fehrle
2021-01-06Merge PR #13563: Revival of #9710 (Compact kernel representation of ↵coqbot-app[bot]
pattern-matching) Reviewed-by: mattam82 Reviewed-by: SkySkimmer Ack-by: gares Ack-by: jfehrle
2021-01-06Merge PR #13714: Changelog for 8.13.0coqbot-app[bot]
Reviewed-by: Zimmi48
2021-01-06[micromega] Add missing support for `implb`BESSON Frederic
2021-01-05[doc] tell sphinxcontrib-bibtex which bibtex file to useEnrico Tassi
2021-01-04Document the change of case representation.Pierre-Marie Pédrot
2021-01-04Changelog for 8.13.0Enrico Tassi
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-29[refman] Clarify meaning of goal in documentation of instantiate.Théo Zimmermann
2020-12-29Document the -native-compiler optionPierre Roux
2020-12-28Merge PR #13665: Set Python's default output encoding to utf-8coqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: palmskog
2020-12-26Set the locale in Docker so Python's default output encoding is utf-8Jim Fehrle
2020-12-21Shorten/improve intro of "Basic proof writing" chapter.Théo Zimmermann
2020-12-16Merge PR #13643: Add -q flag to coqrst python invocation of coqtopcoqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: cpitclaudel
2020-12-16Add -q flag to coqrst python invocation of coqtopLasse Blaauwbroek
This will help with reproducibility for people who have something in their coqrc file. Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2020-12-16Merge PR #13568: Fix #13566: Add checks for invalid occurrences in several ↵Pierre-Marie Pédrot
tactics. Reviewed-by: ppedrot
2020-12-14Adding change log for #13568.Hugo Herbelin
2020-12-14Merge PR #13613: [changes] mark #12765 as experimentalcoqbot-app[bot]
Reviewed-by: Zimmi48
2020-12-14Merge PR #13509: Remove compatibility flag Set Bracketing Last Introduction ↵Pierre-Marie Pédrot
Pattern Reviewed-by: Zimmi48 Reviewed-by: ppedrot
2020-12-13Merge PR #13619: doc: Clarify the status of simpl vs cbncoqbot-app[bot]
Reviewed-by: Zimmi48
2020-12-13Add changelog for #13509.Hugo Herbelin
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
2020-12-13Removing flag "Bracketing Last Introduction Pattern".Hugo Herbelin
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.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 13:54:50 +0000