| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: gares
|
|
Reviewed-by: Zimmi48
Reviewed-by: vbgl
|
|
Reviewed-by: jfehrle
|
|
After #8655
|
|
It was missing `Control.once`.
Fixes coq/ltac2#79
Fixes coq/ltac2#77
|
|
|
|
Reviewed-by: JasonGross
Reviewed-by: Zimmi48
|
|
It seems that this command should be classified as modifying the parser.
Fixes #9419
Thanks to @gares
|
|
Fixes #9418
|
|
Adapt to Coq's new proof mode API
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: CohenCyril
Ack-by: Zimmi48
Ack-by: gares
Reviewed-by: maximedenes
|
|
Reviewed-by: ejgallego
Ack-by: ppedrot
|
|
|
|
|
|
|
|
Reviewed-by: ejgallego
Reviewed-by: gares
Ack-by: maximedenes
|
|
shortening a strict prefix of an application
Reviewed-by: ejgallego
|
|
|
|
This makes it print the warning before the definition message, so if
we run with +non-primitive-record we don't see
"""
defined foo
error could not define foo
"""
|
|
Reviewed-by: gares
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
|
|
|
|
|
|
|
|
|
|
Reviewed-by: maximedenes
|
|
|
|
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.
|
|
Also fold it into `Z.div_mod_to_quot_rem`
Note that the test-suite file is a bit slow. On my machine, it is
```
real 2m32.983s
user 2m32.544s
sys 0m0.492s
```
|
|
Note that we define a `cleanup` tactic which is essential for speed of
reasoning. Perhaps this tactic should make it into the code for
`Z.div_mod_to_quot_rem` somewhere?
```coq
Ltac cleanup :=
repeat match goal with
| [ H : ?T -> _, H' : ?T |- _ ] => specialize (H H')
| [ H : ?T -> _, H' : ~?T |- _ ] => clear H
| [ H : ~?T -> _, H' : ?T |- _ ] => clear H
| [ H : 0 < ?x -> _, H' : ?x < 0 |- _ ] => clear H
| [ H : ?x < 0 -> _, H' : 0 < ?x |- _ ] => clear H
| _ => progress subst
end.
```
|
|
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`.
|
|
Disjunctions seem to have a negative performance impact, so let's try
implications instead.
|
|
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.
|
|
In response to review comments by Zimmi48
|
|
This commit was created via `./dev/tools/update-compat.py --master`
|
|
We now support --master and --release. On the master branch, we support
four compatibility versions, while on releases and release branches, we
support only three compatibility versions.
We also support --git-add to automatically run `git add` with new and
updated files, and to run `git rm` with deleted files.
|
|
The definition of \plus and \tri in cic.rst is not effective
for HTML output.
So, move them into refman-preamble.sty.
Also, \tri is renamed to \trii to express
the suffix of "\triangleright_\iota".
|
|
Reviewed-by: cpitclaudel
|
|
|
|
DAG nodes hold now a system state and a parsing state.
The latter is always passed to the parser.
This paves the way to decoupling the effect of commands on the parsing
state and the system state, and hence never force to interpret, say,
Notation.
Handling proof modes is now done explicitly in the STM, not by interpreting
VernacStartLemma.
Similarly Notation execution could be split in two phases in order to obtain a
parsing state without fully executing it (that requires executing all
commands before it).
Co-authored-by: Maxime Dénès <maxime.denes@inria.fr>
Co-authored-by: Emilio Jesus Gallego Arias <e+git@x80.org>
|
|
|
|
|
|
Ack-by: Zimmi48
Ack-by: anton-trunov
Ack-by: jfehrle
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: maximedenes
|
