aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/proof-engine
AgeCommit message (Expand)Author
2020-05-11Allow to rebind the old value of a mutable Ltac2 entry.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-08Merge PR #12281: [doc] named lemmas can be Saved tooThéo Zimmermann
2020-05-08Merge PR #12121: Fixes #11903 and warns about non truly-recursive (co)fixpointsPierre-Marie Pédrot
2020-05-08doc: one can save named lemmas Save tooAntonio Nikishaev
2020-05-07Documenting the new behavior of "subst".Hugo Herbelin
2020-05-06Moving lazymatch and multimatch to simple identifiers.Hugo Herbelin
2020-05-06Mention keywords from g_ltac.mlg used in Ltac.Hugo Herbelin
2020-05-06Mention keywords used in tactics from g_tactic.mlg.Hugo Herbelin
2020-05-03Merge PR #12197: LtacProf now handles multi-success backtrackingPierre-Marie Pédrot
2020-05-02LtacProf now handles multi-success backtrackingJason Gross
2020-05-01Fixing #11903: Fixpoints not truly recursive in standard library.Hugo Herbelin
2020-05-01Move essential vocabulary and syntax conventions to section on basics.Théo Zimmermann
2020-05-01Remove flags, options and tables from vernac chapter.Théo Zimmermann
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 #12154: [documentation] ssreflect: Abbreviations do not support scopeThéo Zimmermann
2020-04-23[documentation] ssreflect: Abbreviations do not support scopeKenji Maillard
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-23Merge PR #12034: Make cumulative sprop a typing flag, deprecate command line...Pierre-Marie Pédrot
2020-04-21Document changed warnings and erros following #12038.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-17Deprecate “omega”Vincent Laporte
2020-04-16NativeCompute Timing: Use real, not user timeJason Gross
2020-04-16Make cumulative sprop a typing flag, deprecate command line -sprop-cumulativeGaëtan Gilbert
2020-04-11Merge PR #11961: Convert vernac commands chapter to prodn, update syntaxThéo Zimmermann
2020-04-10Convert vernac commands chapter to prodn, update syntaxJim Fehrle
2020-04-07Fix documentation of Print Libraries following #10476.Théo Zimmermann
2020-03-29Merge PR #11944: Remove SearchAbout command, deprecated in 8.5Théo Zimmermann
2020-03-28Remove SearchAbout command, deprecated in 8.5Jim Fehrle
2020-03-28Document change of behavior of Fail in 8.11.Théo Zimmermann
2020-03-25Convert Gallina Extensions to use prodnJim Fehrle
2020-03-19Interpret the Export modifier of Set and Unset as an attribute.Théo Zimmermann
2020-03-19Document all the existing attributes.Théo Zimmermann
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-05Merge PR #11522: Adding an alias `pose proof (x:=t)` for `pose proof t as x` ...Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:46:33 +0000