aboutsummaryrefslogtreecommitdiff
path: root/doc/sphinx/addendum
AgeCommit message (Collapse)Author
2019-02-01Merge PR #8062: Add Z.div_mod_to_quot_rem tactic, put it in zifyVincent Laporte
Ack-by: JasonGross Reviewed-by: fajb Reviewed-by: jfehrle
2019-01-30[toplevel] Deprecate the `-compile` flag in favor of `coqc`.Emilio Jesus Gallego Arias
This PR deprecates the use of `coqtop` as a compiler. There is no point on having two binaries with the same purpose; after the experiment in #8690, IMHO we have a lot to gain in terms of code organization by splitting the compiler and the interactive binary. We adapt the documentation and adapt the test-suite. Note that we don't make `coqc` a true binary yet, but here we take care only of the user-facing part. The conversion of the binary will take place in #8690 and will bring code simplification, including a unified handling of arguments.
2019-01-24Rename Z.div_mod_to_quot_rem, add Z.quot_rem_to_equations, ↵Jason Gross
Z.to_euclidean_division_equations
2019-01-24Revert "Add subst to the end of nia in the test-suite"Jason Gross
This reverts commit b49f4e966443a76ac70d37c4cde68f94de164c01. It turns out the 4x was due to .nia.cache (because I didn't clean sufficiently in testing), not due to `subst`.
2019-01-24Add subst to the end of nia in the test-suiteJason Gross
This speeds up the file from 2m32s to ``` real 0m41.851s user 0m41.512s sys 0m0.376s ``` Also note the `subst` trick in the doc.
2019-01-24Don't bundle Z.div_mod_quot_rem into zifyJason Gross
Alas, I have not had time to work on imrpoving the performance of nia, and there has been a request to include this tactic (which is useful on its own) without bundling it into `zify`. So that is what we do here. I leave the definition of it in `PreOmega` in case we want to eventually include it in `zify`/`nia`.
2019-01-24Add Z.div_mod_to_quot_rem tactic, put it in zifyJason Gross
The various (micr)omega tactics now support `Z.div` and `Z.modulo`. I briefly looked into supporting `Nat.div` and `Nat.modulo`, but the conversions between `Z.div` and `Nat.div` are defined in `ZArith.Zdiv`, which depends on `Omega`, which depends on `PreOmega`, which is where `zify` is defined.
2019-01-22Remove unneeded | in productionlistsJim Fehrle
2018-12-04Add undocumented options from mattam82Jim Fehrle
2018-12-04Document undocumented flags and optionsJim Fehrle
Also remove a few undocumented settings
2018-12-03A few fixes of unexisting tokens.Théo Zimmermann
2018-12-03Closes #9118: single backticks are made equivalent to double backticks; try ↵Théo Zimmermann
to fix all misuses.
2018-11-30Add indexes for coercion / substructure symbol :>.Théo Zimmermann
And a few more Sphinx fixes in passing.
2018-11-28Merge PR #9015: [Typeclasses] Warn when RHS of `:>` is not a classMatthieu Sozeau
2018-11-27Merge PR #8850: Private universes for opaque polymorphic constants.Matthieu Sozeau
2018-11-27[Typeclasses] Warn when RHS of `:>` is not a classVincent Laporte
This introduces the warning “not-a-class” in the “typeclasses” category.
2018-11-25Merge PR #9036: Add bodies to sphinx objects.Clément Pit-Claudel
2018-11-23Doc for Private Polymorphic Universes.Gaëtan Gilbert
2018-11-21[sphinx] Progress towards closing #7602: remove most objects without a body.Théo Zimmermann
Remove objects without body from most chapters. The remaining problems are all in the SSReflect chapter.
2018-11-19Minor update to micromega.rstsoraros
2018-10-09Refactoring of Micromega code using a Simplex linear solverFrédéric Besson
- Simplex based linear prover Unset Simplex to get Fourier elimination For lia and nia, do not enumerate but generate cutting planes. - Better non-linear support Factorisation of the non-linear pre-processing Careful handling of equation x=e, x is only eliminated if x is used linearly - More opaque interfaces (Linear solvers Simplex and Mfourier are independent) - Set Dump Arith "file" so that lia,nia calls generate Coq goals in filexxx.v. Used to collect benchmarks and regressions. - Rationalise the test-suite example.v only tests psatz Z example_nia.v only tests lia, nia In both files, the tests are in essence the same. In particular, if a test is solved by psatz but not by nia, we finish the goal by an explicit Abort. There are additional tests in example_nia.v which require specific integer reasoning out of scope of psatz.
2018-09-25Remove romegaVincent Laporte
2018-09-20Rewrite "Flags, Options and Tables" section.Jim Fehrle
Mark boolean-valued options with :flag: Adjust tactic and command names so parameters aren't shown in the index unless they're needed for disambiguation. Remove references to synchronous options. Revise doc for tables. Correct indentation for text below :flag:
2018-09-20[doc] Fix a few syntax highlighting issuesClément Pit-Claudel
2018-09-20[doc] Include the rst and LaTeX preambles automatically in all filesClément Pit-Claudel
2018-09-20[doc] Remove an empty '.. bibliography::' in addendum/programClément Pit-Claudel
2018-09-11Merge PR #8425: Deprecate romega in favor of liaPierre-Marie Pédrot
2018-09-10Merge PR #8104: Warnings on coercions used without being ImportedEnrico Tassi
2018-09-10Deprecate romega in favor of lia.Vincent Laporte
2018-09-07Recover lost snippetMatěj G
This snippet on pattern matching got lost in the process of migrating to Sphynx.
2018-09-07Warnings on coercions used without being ImportedMaxime Dénès
This warning makes it much easier to stop relying on `Set Automatic Coercions Import`. Tested with success on math-classes.
2018-08-31Fixed the seealso directive in a few places.Zeimer
2018-08-31Uniformized many spelling variants. Added .. warning:: and .. seealso:: ↵Zeimer
directives in many places. Disambiguated terminology: disequality now means <> while inequality means < <= > >=. Fixed some more grammar and spelling issues.
2018-08-03Fix docs on arguments to setoid_replace. Fixes #8213Langston Barrett
2018-08-02Merge PR #8145: Improved grammar and spelling in chapter 'Extended pattern ↵Théo Zimmermann
matching' of the Reference Manual.
2018-08-02Merge PR #8176: Improved grammar and spelling in chapters 'Type Classes', ↵Théo Zimmermann
'Omega' and 'Micromega' of the Reference Manual.
2018-08-01Added a tactic index entry for nsatz, reformatted commands in chapter ↵Zeimer
'Generalized Rewriting' and renamed the chapter Nsatz from _nsatz to _nsatz_chapter.
2018-08-01Improved grammar and spelling in the remaining chapters of the Reference Manual.Zeimer
2018-08-01Improved grammar and spelling in chapter 'Extended pattern matching' of the ↵Zeimer
Reference Manual.
2018-08-01Improved grammar and spelling in chapters 'Type Classes', 'Omega' and ↵Zeimer
'Micromega' of the Reference Manual.
2018-08-01Merge PR #8192: Fix typos and typesetting of doc on ProgramThéo Zimmermann
2018-08-01Merge PR #8184: Improved grammar and spelling in chapters 'Extraction', ↵Théo Zimmermann
'Program' and 'ring and field' chapters of the Reference Manual.
2018-07-30Fix typos and typesetting of doc on ProgramLysxia
2018-07-30[sphinx] Use arguments of '.. example::' directive as a titleClément Pit-Claudel
Most existing uses of .. example did not use the first line as a title, so this commit also adds appropriate blank lines.
2018-07-29Improved grammar and spelling in chapters 'Extraction', 'Program' and 'ring ↵Zeimer
and field' chapters of the Reference Manual.
2018-07-26Improved chapters 'Implicit Coercions' and 'Canonical Structures' of the ↵Zeimer
Reference Manual.
2018-07-17Remove fourier pluginMaxime Dénès
As stated in the manual, the fourier tactic is subsumed by lra.
2018-06-25Merge PR #7559: Existing Class noop when already a class + warning.Matthieu Sozeau
2018-06-19[doc] Use productionlist instead of prodn in ring.rstClément Pit-Claudel
2018-06-13doc: fix typo.whitequark
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 18:45:30 +0000