| Age | Commit message (Collapse) | Author |
|---|
|
- More consistent code indentation
- Nest command variants properly
- Make `Context` explanation a bit less terse, with more links
- Typesetting bits, add some :cmd: links
|
|
|
|
|
|
By default Coq warnings are made fatal when building the manual.
If you want to show a command resulting in a warning, use the warn
option.
Preexisting warnings are either fixed or marked as expected.
|
|
|
|
|
|
|
|
|
|
Ack-by: Zimmi48
|
|
|
|
|
|
Maybe we should still let it run but let's disable it until we install
csdp on the build server at least.
|
|
|
|
|
|
|
|
Ack-by: JasonGross
Reviewed-by: fajb
Reviewed-by: jfehrle
|
|
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.
|
|
Z.to_euclidean_division_equations
|
|
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`.
|
|
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.
|
|
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`.
|
|
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.
|
|
|
|
|
|
Also remove a few undocumented settings
|
|
|
|
to fix all misuses.
|
|
And a few more Sphinx fixes in passing.
|
|
|
|
|
|
This introduces the warning “not-a-class” in the “typeclasses” category.
|
|
|
|
|
|
Remove objects without body from most chapters.
The remaining problems are all in the SSReflect chapter.
|
|
|
|
- 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.
|
|
|
|
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:
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This snippet on pattern matching got lost in the process of migrating to Sphynx.
|
|
This warning makes it much easier to stop relying on `Set Automatic
Coercions Import`. Tested with success on math-classes.
|
|
|
|
directives in many places. Disambiguated terminology: disequality now means <> while inequality means < <= > >=. Fixed some more grammar and spelling issues.
|
|
|
|
matching' of the Reference Manual.
|
