| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
Reviewed-by: SkySkimmer
Reviewed-by: herbelin
|
|
Reviewed-by: herbelin
|
|
Reviewed-by: erikmd
Reviewed-by: herbelin
|
|
Reviewed-by: herbelin
Reviewed-by: maximedenes
|
|
Reviewed-by: Zimmi48
|
|
|
|
|
|
|
|
The first one is encapsulating the clenv part, and is now purely internal,
while the other one provides an abstract interfact to get fresh term instances
from a hint.
|
|
The costly universe refreshing functions were only used for typeclass hint
resolution, which now relies on the provided hint context.
|
|
The old code was refreshing the whole evarmap when only the constraints
introduced by the term would matter. Since exact hints never introduces
metas for missing binders, there is nothing to extract from the clenv,
so we can just generate a fresh universe substitution.
|
|
|
|
We inline the clenv universe refreshing, since it was the only place in the
code that used it. Furthermore it was performing useless substitutions in
the clenv.
|
|
|
|
|
|
|
|
|
|
|
|
It was unnecessarily obfuscated.
|
|
|
|
Reviewed-by: Zimmi48
Ack-by: herbelin
Reviewed-by: ppedrot
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
Reviewed-by: vbgl
|
|
Reviewed-by: vbgl
|
|
Reviewed-by: CohenCyril
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: maximedenes
Ack-by: ppedrot
|
|
zify used to generate many syntactic positivity constraints when translating a goal
from nat to Z. For instance, to state that the product of 2 integers
is positive. Instead, lia performs an interval analysis that is more semantic.
The bug was that the interval analysis was performed after the
elimination of equations. The current workaround is to perform
interval analysis before and after eliminating equations.
bla
|
|
The elimination of let bindings is performing a convertibility check in
order to deal with type aliases.
|
|
|
|
We also put them in a module, so users can `Require Int63. Import
Int63.Int63Notations` without needing to unqualify the primitives.
In particular, we change
- `a \% m` into `a mod m` to correspond with the notation in ZArith
- `m == n` into `m =? n` to correspond with the eqb notations elsewhere
- `m < n` into `m <? n` to correspond with the ltb notations elsewhere
- `m <= n` into `m <=? n` to correspond with the leb notations elsewhere
- `m ≤ n` into `m ≤? n` for consistency with the non-unicode notation
The old notations are still accessible as deprecated notations.
Fixes #12454
|
|
This is a companion to #12479 as per
https://github.com/coq/coq/pull/12479#issuecomment-641336039 that
changes some of the PrimFloat notations:
- `m == n` into `m =? n` to correspond with the eqb notations elsewhere
- `m < n` into `m <? n` to correspond with the ltb notations elsewhere
- `m <= n` into `m <=? n` to correspond with the leb notations elsewhere
We also put them in a module, so users can `Require PrimFloat. Import
PrimFloat.PrimFloatNotations` without needing to unqualify the
primitives.
Fixes the part of #12454 about floats
|
|
Reviewed-by: vbgl
|
|
Since this PR, ocamlfind looks for num when building plugins.
To avoid requiring all plugins to add a new, irrelevant, dependency, we propagate it.
This solution imitates what was decided for nixpkgs in NixOS/nixpkgs#94230.
Fix coq-community/aac-tactics#61.
|
|
environment variable
Reviewed-by: Zimmi48
Ack-by: jfehrle
|
|
read.
Reviewed-by: jfehrle
Ack-by: Mbodin
Ack-by: corwin-of-amber
|
|
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
|
|
|
|
Reviewed-by: Zimmi48
|
|
|
|
Reviewed-by: Zimmi48
Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: jtcoolen
|
|
This allows coqbot to reply back with a minimized
version of some code reproducing a bug, using the
coq-bug-minimizer program from Jason Gross.
See https://github.com/JasonGross/coq-tools#coq-bug-minimizer.
|
|
|
|
Reviewed-by: Lysxia
|
|
Reviewed-by: Zimmi48
|
|
The change introduced by 41a1d66 has broken the feature prior to its
initial release. We attempt to fix the issue, and add a comment to
warn feature developers in order to avoid facing the same issue again.
|
|
The tactics do in SSReflect uses `? @mult` rather than `? @num`.
|
|
Reviewed-by: Lysxia
|
|
The old API was taking a function to decompose constr patterns into dnet
patterns, but it was applying it in an eager way. So there is not point in
exposing such a complex interface. Instead, we make explicit the dnet pattern
type, export a function that turns a constr pattern into a dnet pattern, and
make the add and remove dnet functions take a dnet pattern instead.
This only affects pattern-consuming functions. The lookup function, which
operates on kernel terms instead of constr patterns, is still relying on HO
primitives.
|
|
minimization.
Reviewed-by: SkySkimmer
|
