aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/proof-engine
AgeCommit message (Collapse)Author
2020-06-17tactics.rst: readd `cbv`Paolo G. Giarrusso
Hope this is enough, also looking at https://github.com/coq/coq/commit/4c9ba141f8f7e067f274cb5a02293e8e52f89487#diff-a907eea979c6d310cb6208180b556d6d.
2020-06-08Convert Ltac chapter to prodnJim Fehrle
2020-06-08Make automatic name generation for directives more consistent:Jim Fehrle
- by default, generate names for all directives using the prefix "[a-zA-Z0-9_ ]+" except - don't generate a name for cmdv and tacv - generate more flexibily for exn, warn and attr
2020-06-04Tweak wording.Théo Zimmermann
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-06-04Document known issue of Proof <term> with PG.Théo Zimmermann
See #12444.
2020-05-16Merge PR #8855: More search optionsEmilio Jesus Gallego Arias
Reviewed-by: SkySkimmer Ack-by: Zimmi48 Ack-by: ejgallego Ack-by: kyoDralliam
2020-05-15Merge PR #12239: Split Gallina, Gallina ext and most of CIC chapters into ↵Clément Pit-Claudel
multiple pages. Reviewed-by: jfehrle
2020-05-15Document new Search features.Théo Zimmermann
2020-05-14Add some markers of origin.Théo Zimmermann
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
Reviewed-by: Zimmi48 Reviewed-by: jfehrle Ack-by: ppedrot
2020-05-12Merge PR #11503: Allow to rebind the old value of a mutable Ltac2 entry.Jason Gross
Reviewed-by: JasonGross Ack-by: Zimmi48 Ack-by: kyoDralliam
2020-05-12Merge PR #12146: Fixes #10812: tactic subst failure with section variables ↵Pierre-Marie Pédrot
indirectly dependent in goal Ack-by: Zimmi48 Reviewed-by: ppedrot
2020-05-12documenting with examples the dynamic behaviour of Ltac2 SetKenji Maillard
2020-05-11Correcting ltac2's documentation on values turning test into proper check.Kenji Maillard
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
This reverts commit 3c66c60e52b334482bcfe3d1d97bb77e4d011d18. We instead add a warning in the manual and a kludge in the test-suite.
2020-05-09[with_strategy] Work around #12191Jason Gross
2020-05-09Work around a bug in Coq in the docJason Gross
This is the bug https://github.com/coq/coq/pull/12129#issuecomment-619613779
2020-05-09Elaborate with_strategy warningJason Gross
As per https://github.com/coq/coq/pull/12129#issuecomment-619389803 Note that we need to work around #12179 in doc of with_strategy
2020-05-09Fix the `with_strategy` tactic to work with `abstract`Jason Gross
2020-05-09Add a `with_strategy` tacticJason Gross
Useful for guarding calls to `unfold` or `cbv` to ensure that, e.g., `Opaque foo` doesn't break some automation which tries to unfold `foo`. We have some timeouts in the strategy success file. We should not run into issues, because we are not really testing how long these take. We could just as well use `Timeout 60` or longer, we just want to make sure the file dies more quickly rather than taking over 10^100 steps. Note that this tactic does not play well with `abstract`; I have a potentially controversial change that fixes this issue. One of the lines in the doc comes from https://github.com/coq/coq/pull/12129#issuecomment-619771556 Co-Authored-By: Pierre-Marie Pédrot <pierre-marie.pedrot@irif.fr> Co-Authored-By: Théo Zimmermann <theo.zimmermann@inria.fr> Co-Authored-By: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com>
2020-05-08Merge PR #12281: [doc] named lemmas can be Saved tooThéo Zimmermann
Reviewed-by: Zimmi48
2020-05-08Merge PR #12121: Fixes #11903 and warns about non truly-recursive (co)fixpointsPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2020-05-08doc: one can save named lemmas Save tooAntonio Nikishaev
2020-05-07Documenting the new behavior of "subst".Hugo Herbelin
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
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
Ack-by: Zimmi48 Reviewed-by: ppedrot
2020-05-02LtacProf now handles multi-success backtrackingJason Gross
Fixes #12196
2020-05-01Fixing #11903: Fixpoints not truly recursive in standard library.Hugo Herbelin
There was also a non truly recursive in the doc.
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
Ack-by: JasonGross Ack-by: Zimmi48 Ack-by: cpitclaudel
2020-04-27Merge PR #12132: [refman] Remove references to omega from Tactics chapter.Vincent Laporte
Reviewed-by: vbgl
2020-04-26Convert syntax extensions chapter to prodnJim Fehrle
2020-04-26Merge PR #12176: Doc: extend example for induction a bitThéo Zimmermann
Reviewed-by: Zimmi48
2020-04-25Doc: extend example for induction a bitGaëtan Gilbert
This makes it show the shape of the induction hypothesis in the second goal instead of just saying "subgoal 2 is S n <= S n".
2020-04-23Merge PR #12154: [documentation] ssreflect: Abbreviations do not support scopeThéo Zimmermann
Ack-by: Zimmi48 Reviewed-by: gares
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
Reviewed-by: jfehrle
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 ↵Pierre-Marie Pédrot
line -sprop-cumulative Reviewed-by: Zimmi48 Reviewed-by: ppedrot
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
Omega was defined twice and this is the tactics chapter documentation which was refered to from the tactic index. We remove it so that users find the other reference (which contains the deprecation notice). The changes to the doc of zarith are a follow-up to #11976.
2020-04-20Remove funind tactics from Tactics chapter.Théo Zimmermann
2020-04-17Deprecate “omega”Vincent Laporte
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 07:41:11 +0000