aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx
AgeCommit message (Collapse)Author
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 #12268: Add an example to motivate strictly positive occurrences checkThé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-07Drop some the coqtop output, rephrase a bitQuentin Carbonneaux
2020-05-06Add an example to motivate strictly positive occurrences checkQuentin Carbonneaux
2020-05-05[refman] Add missing (only parsing) to example of compat notations.Théo Zimmermann
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-01Preserve vernac chapter.Théo Zimmermann
2020-05-01Extract two new files out of Gallina chapter.Théo Zimmermann
2020-05-01Create section on writing libraries with only deprecated attributes.Théo Zimmermann
2020-05-01Extract deprecated attribute from Gallina chapter.Théo Zimmermann
2020-05-01Remove flags, options and tables from vernac chapter.Théo Zimmermann
2020-05-01Remove lexical conventions and attributes from Gallina chapter.Théo Zimmermann
2020-05-01Create basics out of sections from Gallina and Vernac chapters.Théo Zimmermann
2020-05-01Create section on basics with just flags, options and tables.Théo Zimmermann
2020-05-01Extract flags, options and tables from vernac chapter.Théo Zimmermann
2020-05-01Create section on basics with just lexical conventions and attributes.Théo Zimmermann
2020-05-01Extract lexical conventions and attributes from Gallina chapter.Théo Zimmermann
2020-04-29Merge PR #11606: [tools] Add memory stats to tables by defaultEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-04-29Merge PR #12150: Support in-line glossary definitions and references with an ↵Clément Pit-Claudel
index Ack-by: Zimmi48
2020-04-29Support in-line glossary entries and referencesJim Fehrle
with an index
2020-04-28Merge PR #12183: Suggestion of improvement for the Allow SProp error message.Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: jfehrle
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 #12090: Remove documentation for Hide menu in CoqIDE (was removed ↵Clément Pit-Claudel
in 8.5).
2020-04-27Merge PR #12132: [refman] Remove references to omega from Tactics chapter.Vincent Laporte
Reviewed-by: vbgl
2020-04-27Further documentation improvements.Théo Zimmermann
2020-04-27Improve the Allow SProp error message.Théo Zimmermann
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-24Add memory stats to tables by defaultJason Gross
The Python scripts now support `--no-include-mem` to turn it off, and also support `--sort-by-mem`. Closes #11575
2020-04-24Merge PR #12156: Document `+` in polymorphic universe levelsThéo Zimmermann
Reviewed-by: Zimmi48
2020-04-23Merge PR #12154: [documentation] ssreflect: Abbreviations do not support scopeThéo Zimmermann
Ack-by: Zimmi48 Reviewed-by: gares
2020-04-23Merge PR #12117: Make multiplication of Cauchy reals transparent and ↵Hugo Herbelin
accelerate it Reviewed-by: herbelin
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-22Merge PR #11928: Remove probably useless doc/sphinx/coqdoc.css.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 15:43:01 +0000