| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Close #12909
|
|
Reviewed-by: ppedrot
|
|
The purpose of `NsatzTactic` is to allow using `nsatz` without the
dependency on real axioms. So we declare the instances for `Z` and `Q`
in that file, so that users don't have to re-create them.
Fixes #12860
|
|
Reviewed-by: Zimmi48
|
|
Fix #12676
|
|
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
Reviewed-by: SkySkimmer
|
|
Fix #12889
|
|
|
|
|
|
Reviewed-by: ejgallego
|
|
documentation
Reviewed-by: SkySkimmer
Reviewed-by: herbelin
Reviewed-by: jfehrle
|
|
Reviewed-by: mattam82
Ack-by: ppedrot
|
|
Reviewed-by: SkySkimmer
|
|
exist
Reviewed-by: SkySkimmer
|
|
of artificial dependencies disappearing by reduction
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Reviewed-by: herbelin
|
|
Reviewed-by: ppedrot
|
|
be added
Reviewed-by: CohenCyril
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
Ack-by: gares
|
|
|
|
We fix it by reducing K-redexes the same in the both places
(make_tuple and minimal_free_rels) which compute the dependencies of a
dependent equality.
|
|
Amends c1b1afe76e1655cc3275bdf4215f0ab690efc3cc
|
|
Reviewed-by: herbelin
Reviewed-by: maximedenes
|
|
|
|
It now silently does nothing rather than erroring with `mv: cannot stat
'output/*.out.real': No such file or directory` if there is no output to
approve, and also correctly handles `output-coqtop` and `output-coqchk`
rather than ignoring these directories.
Fixes #12863
|
|
Fixes #12845 (coqchk reports names from inner modules of opaque modules
as axioms)
I don't fully understand the code here, so I can't speak as to its
correctness, but it should be simple enough that reviewers can
understand what it's doing and whether or not it's correct.
This is useful for me in making progress towards
https://github.com/mit-plv/fiat-crypto/issues/736
|
|
When calling an Ltac function, add specific locations when
interpreting the function, when interpreting the arguments and when
executating the call (in a TacArg).
|
|
Try just going with the user-given names, and not worrying about
what happens with repeated names or anonymous implicits.
(Support for anonymous implicits is due to herbelin in #11098.)
This PR should not change behaviour in the absence of repeated names.
Since repeated names are already a poorly handled corner case, I would
recommend changing binder names to avoid overlap in the case of a
change in behavior.
Since anonymous implicits and implicits with repeated names can already
happen, I think this is unlikely to cause too many new problems,
though it might exacerbate existing ones. However, I already had to fix
one newly possible anomaly, so I can't be too confident.
The most common change in external developments was that an argument
no longer gets `0` appended to it, causing the `Arguments` command
to complain about renaming.
To fix this and keep the old name, one can simply use the `rename` flag
as suggested, or switch to the new, un-suffixed name.
Closes #6785
Closes #12001
Another step towards checking the standard library with `-mangle-names`.
|
|
test files.
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Co-authored-by: Hugo Herbelin <Hugo.Herbelin@inria.fr>
|
|
The directory is obsolete since 7461fe4f.
|
|
Fix #7015
|
|
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`.
|
|
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: erikmd
Reviewed-by: herbelin
|
|
Reviewed-by: herbelin
Reviewed-by: maximedenes
|
|
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
|
|
|
|
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.
|
|
Defined constants
Reviewed-by: ppedrot
|
|
Fix #12742
|
