| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Reviewed-by: mattam82
|
|
Ack-by: SkySkimmer
Reviewed-by: gares
|
|
Reviewed-by: ppedrot
|
|
The update of a loc needs sometimes to override (when calling an Ltac
function), and otherwise to keep the existing loc (assumed to be
fined). We refine this (see e.g. the ErrorLocation_tac_in_term tests).
Moreover, when overriding, this was going to a tclOR backtracking
point which was setting the loc to a completely disjoint part of the
code having caused the error (see #12773). We replace the tclOR by a
tclORELSE.
|
|
Reviewed-by: jfehrle
Reviewed-by: ppedrot
|
|
construct
Reviewed-by: Zimmi48
Ack-by: gares
Ack-by: jfehrle
|
|
As suggested by Laurent Thery to Chris Dams on Coq-Club.
(And fix the documented syntax in the manual.)
|
|
purely applicative stacks
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
|
|
Due to the way transparency is handled in hint databases, every time it is
changed, all dnets are recomputed from scratch. This is very expensive, and
a bench showed that it was sometimes contributing significantly to the whole
compilation time of hint-heavy libraries. This patch makes this computation
lazy, so that the dnet is computed only the first time a hint lookup is
performed.
The implementation is functionally equivalent to wrapping the sentry_bnet
field in a Lazy.t, but because dnets are stored in the summary and thus
marshalled, I had to manually perform a defunctionalization.
A (maybe cleaner?) alternative would be to track the set of constants a
hint depend on, in order to only refresh those touched by the change of
transparency. Yet, this would be a much more invasive change.
|
|
Reviewed-by: gares
|
|
Reviewed-by: anton-trunov
|
|
Reviewed-by: anton-trunov
|
|
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.
|
|
Co-authored-by: Anton Trunov <anton.a.trunov@gmail.com>
|
|
|
|
|
|
|
|
Reviewed-by: Zimmi48
Ack-by: herbelin
Reviewed-by: ppedrot
|
|
Probably a remnant of a time where the difference in code path was relevant.
|
|
It was only used there, and its API required to export an ad-hoc type
to represent pattern-matchings.
|
|
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
|
