aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/proof-engine
AgeCommit message (Collapse)Author
2020-09-18Make `simple apply in ...` point to `simple apply`Maxime Dénès
Instead, the example was duplicated.
2020-09-18Improve `simple apply` exampleMaxime Dénès
The example showing the difference between `apply` and `simple apply` used to depend on the order and the heuristics used on unification problems. We make it independent for better clarity and stability. Fixes https://github.com/coq/coq/issues/13023
2020-09-11Turn integer into natural in several mlgsPierre Roux
Negative values had no meaning there. Those were spotted by Hugo Herbelin while reviewing #12979 .
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
num stands for natural numbers whereas the text deals with negative values.
2020-09-11Minimal changes to make the refman compatible with Sphinx 3.Théo Zimmermann
Co-authored-by: Jim Fehrle <jfehrle@sbcglobal.net>
2020-09-08Merge PR #12993: Remove deprecated tactic cutrewrite.Clément Pit-Claudel
Reviewed-by: cpitclaudel Reviewed-by: ppedrot
2020-09-08Remove deprecated tactic cutrewrite.Théo Zimmermann
2020-09-08Merge PR #12931: Proof using cleanup, small doc addition and fix using Type ↵coqbot-app[bot]
in collections Reviewed-by: gares Ack-by: Zimmi48
2020-09-07Explain how selectors change the order of goalsJim Fehrle
2020-08-28Proof using cleanup, small doc addition and fix using Type in collectionsGaëtan Gilbert
Fix #12930
2020-08-26Merge PR #12085: Convert ltac2 chapter to use prodn, update syntaxcoqbot-app[bot]
Reviewed-by: JasonGross Reviewed-by: Zimmi48 Ack-by: jfehrle Ack-by: ppedrot
2020-08-25Convert ltac2 chapter to use prodn, update syntaxJim Fehrle
2020-08-17Recommend replace as a replacement to cutrewrite.Théo Zimmermann
As suggested by Laurent Thery to Chris Dams on Coq-Club. (And fix the documented syntax in the manual.)
2020-08-10Merge PR #12749: [ssr] turn "nothing to inject" into a real warning (fix #12746)Cyril Cohen
Reviewed-by: CohenCyril Reviewed-by: SkySkimmer Ack-by: Zimmi48 Ack-by: maximedenes Ack-by: ppedrot
2020-08-10[ssr] turn "nothing to inject" into a real warning (fix #12746)Enrico Tassi
2020-08-07Merge PR #12643: Document "Print Debug GC" command and OCAMLRUNPARAM ↵coqbot
environment variable Reviewed-by: Zimmi48 Ack-by: jfehrle
2020-08-04Document "Print Debug GC" command and OCAMLRUNPARAM env variableJim Fehrle
2020-07-29Fix do in ssreflect-proof-language.rstYusuke Matsushita
The tactics do in SSReflect uses `? @mult` rather than `? @num`.
2020-07-11tactics.rst: `Require A` is enough for `A`'s hintsPaolo G. Giarrusso
As the text says later: > Hints should only be made available when the module they are defined in is imported, not just required.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 21:19:42 +0000