aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/addendum
AgeCommit message (Collapse)Author
2021-04-21Merge PR #13911: Remove the :> type cast?coqbot-app[bot]
Reviewed-by: mattam82 Ack-by: Zimmi48
2021-04-16[zify] bugfixFrederic Besson
- to zify the conclusion, we are using Tactics.apply (not rewrite) Closes #11089 - constrain the arguments of Add Zify X to be GlobRef.t Unset Primitive Projections so that projections are GlobRef.t. Closes #14043 Update doc/sphinx/addendum/micromega.rst Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2021-04-02Remove the omega tactic and related optionsJim Fehrle
2021-03-30Remove the :> type castJim Fehrle
2021-03-08Convert 2nd part of rewriting chapter to prodnJim Fehrle
2021-01-28Merge PR #13781: [micromega] Deprecate hopefully useless options and flagscoqbot-app[bot]
Reviewed-by: Zimmi48 Ack-by: jfehrle
2021-01-26Merge PR #13758: Remove the Hide Obligations flag (deprecated in 8.12)coqbot-app[bot]
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48
2021-01-25Remove the Hide Obligations flagJim Fehrle
2021-01-25Update doc/sphinx/addendum/micromega.rstFrédéric Besson
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2021-01-22[micromega] Deprecate hopefully useless options and flagsBESSON Frederic
The goal is to eventually only use the Simplex solver and remove all the code needed for fourier elimination.
2021-01-19Remove Add InjTyp and 10 other micromega commandsJim Fehrle
2021-01-18Merge PR #13705: Improve documentation of rewrite_strat/innermost and outermostcoqbot-app[bot]
Reviewed-by: JasonGross Reviewed-by: Zimmi48 Ack-by: gares
2021-01-06Improve description of rewrite_strat/innermost and outermostJim Fehrle
2020-12-30Convert rewriting and proof-mode chapters to prodnJim Fehrle
2020-11-24Convert auto chapter to prodnJim Fehrle
2020-11-20Use nat_or_var where negative values don't make senseJim Fehrle
2020-11-18[attributes] Update error message referring to deprecated syntax.Emilio Jesus Gallego Arias
2020-11-18Review commit: improving the doc of boolean attributes.Théo Zimmermann
2020-11-18[attributes] Deprecate `attr(true)` syntax in favor of booelan attributes.Emilio Jesus Gallego Arias
We introduce a warning so boolean attributes are expected to be of the form `attr={yes,no}` or just `attr` (for `yes`). We update the documentation, test-suite, and changelog.
2020-11-17Merge PR #12653: Syntax for specifying cumulative inductivescoqbot-app[bot]
Reviewed-by: mattam82 Reviewed-by: maximedenes Reviewed-by: jfehrle Ack-by: gares Ack-by: Zimmi48 Ack-by: ppedrot
2020-11-16Merge PR #13188: Default disable automatic generalization of Instance typePierre-Marie Pédrot
Ack-by: Blaisorblade Reviewed-by: JasonGross Reviewed-by: Zimmi48 Ack-by: jfehrle Reviewed-by: ppedrot
2020-11-16Doc for variance syntaxGaëtan Gilbert
2020-11-15Doc and changelog for Instance Generalized OutputGaëtan Gilbert
2020-11-14Distinguish one_pattern and one_term nonterminalsJim Fehrle
2020-11-10Convert logic.rst to prodnJim Fehrle
2020-11-09[refman] Stop applying a special style to Coq, CoqIDE, OCaml and Gallina.Théo Zimmermann
The smallcaps rendering was inexistent in the PDF version and did not look good in the HTML version.
2020-11-09Remove virtually unused replace rule.Théo Zimmermann
2020-11-05Change the title of the automatic tactic chapter and of its sections.Théo Zimmermann
Prefer the term 'solver' to 'decision procedure'.
2020-10-24Convert misc chapters to prodnJim Fehrle
2020-10-22Merge PR #11924: Add style for smallcaps.coqbot-app[bot]
Reviewed-by: jfehrle
2020-10-20Add some missing smallcaps.Théo Zimmermann
2020-10-20[zify] Use flag for Z.to_euclidean_division_equations.Frédéric Besson
Update doc/sphinx/addendum/micromega.rst Co-authored-by: Jason Gross <jasongross9@gmail.com> Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-10-20[zify] Add support for Int63.intFrédéric Besson
Update doc/sphinx/addendum/micromega.rst Co-authored-by: Jason Gross <jasongross9@gmail.com> Update theories/micromega/ZifyInt63.v Co-authored-by: Jason Gross <jasongross9@gmail.com>
2020-10-02{new,setoid_}ring -> ringMaxime Dénès
I believe this renaming makes it easier for new contributors to discover the code of `ring`.
2020-09-27Reduce nitpick_ignore list a little.Théo Zimmermann
2020-09-11[refman] Rename num to naturalPierre Roux
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-03Merge PR #12953: Add :math: around mathcoqbot-app[bot]
Reviewed-by: jfehrle Ack-by: JasonGross
2020-08-30Add :math: around mathJason Gross
2020-08-30Fix rendering of -> in micromegaJason Gross
2020-08-25Require NsatzTactic: nsatz support for Z and QJason Gross
The purpose of `NsatzTactic` is to allow using `nsatz` without the dependency on real axioms. So we declare the instances for `Z` and `Q` in that file, so that users don't have to re-create them. Fixes #12860
2020-08-19Fixes #10902 by adding a mention of the JSON extraction in the documentation.Martin Bodin
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-07-01UIP in SPropGaëtan Gilbert
2020-06-20Add a pre-hook mechanism for the `zify` tacticKazuhiko Sakaguchi
2020-06-14Update zify documentationFrédéric Besson
Add Zify <X> are documented. Add <X> is deprecated as it clashed with the standard Add command
2020-06-14[micromega] native support for boolean operatorsFrédéric Besson
The syntax of formulae is extended to support boolean constants (true, false), boolean operators Bool.andb, Bool.orb, Bool.implb, Bool.negb, Bool.eqb and comparison operators Z.eqb, Z.ltb, Z.gtb, Z.leb and Z.ltb.
2020-06-09Minor improvements to the section on sorts.Théo Zimmermann
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-05-16Add redirects for HTML pages that were moved.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:37:14 +0000