aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/proof-engine/tactics.rst
AgeCommit message (Expand)Author
2020-09-18Make `simple apply in ...` point to `simple apply`Maxime Dénès
2020-09-18Improve `simple apply` exampleMaxime Dénès
2020-09-11[refman] Rename int to integerPierre Roux
2020-09-11[refman] Rename num to naturalPierre Roux
2020-09-11[refman] Replace num by intPierre Roux
2020-09-11Minimal changes to make the refman compatible with Sphinx 3.Théo Zimmermann
2020-09-08Merge PR #12993: Remove deprecated tactic cutrewrite.Clément Pit-Claudel
2020-09-08Remove deprecated tactic cutrewrite.Théo Zimmermann
2020-09-07Explain how selectors change the order of goalsJim Fehrle
2020-08-26Merge PR #12085: Convert ltac2 chapter to use prodn, update syntaxcoqbot-app[bot]
2020-08-25Convert ltac2 chapter to use prodn, update syntaxJim Fehrle
2020-08-17Recommend replace as a replacement to cutrewrite.Théo Zimmermann
2020-08-10[ssr] turn "nothing to inject" into a real warning (fix #12746)Enrico Tassi
2020-07-11tactics.rst: `Require A` is enough for `A`'s hintsPaolo G. Giarrusso
2020-06-17tactics.rst: readd `cbv`Paolo G. Giarrusso
2020-06-08Convert Ltac chapter to prodnJim Fehrle
2020-05-15Merge PR #12239: Split Gallina, Gallina ext and most of CIC chapters into mul...Clément Pit-Claudel
2020-05-14Reintroduce leftover parts; update index files; small fixes.Théo Zimmermann
2020-05-14Remove an outdated piece of documentation about limitations of unfold.Pierre-Marie Pédrot
2020-05-13Merge PR #12229: Hopefully consensual cleaning of keywordsThéo Zimmermann
2020-05-12Merge PR #12146: Fixes #10812: tactic subst failure with section variables in...Pierre-Marie Pédrot
2020-05-09Revert "[with_strategy] Fix for coqchk"Jason Gross
2020-05-09[with_strategy] Work around #12191Jason Gross
2020-05-09Work around a bug in Coq in the docJason Gross
2020-05-09Elaborate with_strategy warningJason Gross
2020-05-09Fix the `with_strategy` tactic to work with `abstract`Jason Gross
2020-05-09Add a `with_strategy` tacticJason Gross
2020-05-07Documenting the new behavior of "subst".Hugo Herbelin
2020-05-06Mention keywords used in tactics from g_tactic.mlg.Hugo Herbelin
2020-04-28Merge PR #11718: Convert syntax extensions chapter to prodnThéo Zimmermann
2020-04-27Merge PR #12132: [refman] Remove references to omega from Tactics chapter.Vincent Laporte
2020-04-26Convert syntax extensions chapter to prodnJim Fehrle
2020-04-26Merge PR #12176: Doc: extend example for induction a bitThéo Zimmermann
2020-04-25Doc: extend example for induction a bitGaëtan Gilbert
2020-04-23Merge PR #12148: Consolidate funind documentation onto a single page.Clément Pit-Claudel
2020-04-23[refman] Fix name of tactic: function induction -> functional induction.Théo Zimmermann
2020-04-23Fix coq snippets in Tactics chapter.Théo Zimmermann
2020-04-20[refman] Remove references to omega from Tactics chapter.Théo Zimmermann
2020-04-20Remove funind tactics from Tactics chapter.Théo Zimmermann
2020-04-16NativeCompute Timing: Use real, not user timeJason Gross
2020-04-10Convert vernac commands chapter to prodn, update syntaxJim Fehrle
2020-03-25Convert Gallina Extensions to use prodnJim Fehrle
2020-03-19firstorder: default tactic is “auto with core”Vincent Laporte
2020-03-18Add documentation for the export hint.Pierre-Marie Pédrot
2020-03-09Remove some productionlistsJim Fehrle
2020-03-05Merge PR #7791: Deprecating the declaration of arbitrary terms as hints.Maxime Dénès
2020-03-03Adding an alias "pose proof (x:=a)" for "pose proof a as x".Hugo Herbelin
2020-02-28Convert Gallina Vernac to use prodnJim Fehrle
2020-02-28Adapt the documentation after deprecation of term hints.Pierre-Marie Pédrot
2020-02-13[build] Consolidate stdlib's .v files under a single directory.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 17:41:41 +0000