| Age | Commit message (Collapse) | Author |
|---|
|
OUnit package name is changed from "oUnit" to "ounit2":
https://github.com/gildor478/ounit#user-content-transition-to-ounit2
This change follows it and fixes
a failure, `ocamlfind: Package oUnit not found`,
at `make test-suite` and `dune build`.
|
|
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
|
|
|
|
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
|
|
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>
|
|
|
