| Age | Commit message (Collapse) | Author |
|---|
|
This feature makes it possible to tell type inference to type
applications of a global `foo` using typing information from the context
once the `n` first arguments are known.
The syntax is: `Arguments foo x y | z`.
Closes #7910
|
|
Reviewed-by: Zimmi48
|
|
|
|
|
|
* use mixfix `(p1 | … | pn)` notation for nested disjunctive patterns,
rather than infix `|`, making pattern syntax consistent with term
syntax.
* disable extending `pattern` grammar with notation incompatible with
the nested disjunctive pattern syntax `(p1 | … | pn)`, such as the `(p
| q)` divisibility notation used by `Numbers`.
* emit a (disabled by default) `disj-pattern-notation` warning when such
`Notation` is attempted.
* update documentation accordingly; document incompatibilities in
`changelog`.
* comment special treatment of `(num)` in grammar.
* update file extensions in `Pcoq` header comment.
* correct the keyword declarations to reflect the contents of the
grammar files; perhaps there should be an option to disable implicit
keyword extension in a `.mlg` file, so that these lists could actually
be checked.
* parse the `|}` manifest record terminator as `|` followed by `}`,
eliminating the `|}` token which conflicts with notations that use `|`
as a terminator (such as, absolute value, norm, or cardinal in
MathComp). Since `|` is now an `operconstr` _and_ `pattern` terminator,
`bar_cbrace` rule checks for contiguous symbols, this change entails no
visible behaviour change.
|
|
|
|
prevent them from being “canonical”
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: gares
Ack-by: maximedenes
Ack-by: robbertkrebbers
Ack-by: vbgl
|
|
|
|
Attributes that enable/disable a feature can have an explicit value
(default is enable when the attribute is present).
Three-valued boolean attributes do not support this:
what would `#[local(false)]` mean?
|
|
frequently on CI.
Reviewed-by: vbgl
|
|
(Merge of the initial version with #9983 was broken)
|
|
|
|
|
|
Previsouly, it was silently ignored.
|
|
|
|
Async causes output reordering in one test. Since we don't care about
the output of that test (it's just a [Fail]) we move it to success/.
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: herbelin
Ack-by: ppedrot
Ack-by: proux01
|
|
This removes various compatibility notations.
Closes #8374
This commit was mostly created by running `./dev/tools/update-compat.py
--release`. There's a bit of manual spacing adjustment around all of the
removed compatibility notations, and some test-suite updates were done
manually.
The update to CHANGES.md was manual.
|
|
|
|
RealField.v is slightly modified so that the ring/field tactics
consider the term (IZR (Z.pow_pos 10 _)) produced when parsing
exponents as constants.
|
|
|
|
This fixes an incompleteness of subtyping on cumulative inductives,
where I@{i} A <= I@{j} A should imply i <= j, i = j or no relation
depending on the variance of I's universe.
|
|
|
|
Prevent errors when under annotating binders.
|
|
|
|
For nonsquashed:
Either
- 0 constructors
- primitive record
|
|
Note currently it's impossible to define inductives in SProp because
indtypes.ml and the pretyper aren't fully plugged.
|
|
|
|
This is because it can raise Not_found in depth and we need to catch
it at the right time.
|
|
This work makes it possible to take advantage of a compact
representation for integers in the entire system, as opposed to only
in some reduction machines. It is useful for heavily computational
applications, where even constructing terms is not possible without such
a representation.
Concretely, it replaces part of the retroknowledge machinery with
a primitive construction for integers in terms, and introduces a kind of
FFI which maps constants to operators (on integers). Properties of these
operators are expressed as explicit axioms, whereas they were hidden in
the retroknowledge-based approach.
This has been presented at the Coq workshop and some Coq Working Groups,
and has been used by various groups for STM trace checking,
computational analysis, etc.
Contributions by Guillaume Bertholon and Pierre Roux <Pierre.Roux@onera.fr>
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
|
|
Ack-by: JasonGross
Reviewed-by: fajb
Reviewed-by: jfehrle
|
|
Reviewed-by: gares
Reviewed-by: mattam82
Reviewed-by: ppedrot
|
|
|
|
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`.
|
|
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.
|
|
This commit was created via `./dev/tools/update-compat.py --master`
|
|
|
|
|
|
- The head of "in" was wrongly considered binding
- Aliases in the "in" pattern were not taken into account
|
|
|
|
|
|
|
|
It seems we started doing the export silently in
47804492bd09c8b13b5aac45800d067dbdf04d00.
|
|
|
|
|
