| Age | Commit message (Collapse) | Author |
|---|
|
preserve the order
Reviewed-by: Zimmi48
Ack-by: chdoc
Ack-by: jfehrle
|
|
The test is refined to handle aliases: i.e. undefined evars coming from
restrictions and evar-evar unifications with an initial evar are not
considered fresh unresolved evars. To check this, we generalize the
restricted_evars set to an aliased_evars set in the evar map,
registering evars being solved by another evar due to restriction
or evar-evar unifications. This implements the proposal of PR #370
for testing the resolution status of evars independently of the evar-evar
orientation order.
This allows [apply] to refine an evar with a new one if it results from a
[clear] request or an evar-evar solution only, otherwise the new evar is
considered fresh and an error is raised.
Also fixes bugs #4095 and #4413.
Co-authored-by: Maxime Dénès <maxime.denes@inria.fr>
|
|
|
|
|
|
Reviewed-by: jfehrle
Ack-by: JasonGross
|
|
|
|
|
|
|
|
|
|
Fix #12930
|
|
|
|
Reviewed-by: ppedrot
Reviewed-by: proux01
|
|
Reviewed-by: JasonGross
Reviewed-by: Zimmi48
Ack-by: jfehrle
Ack-by: ppedrot
|
|
+ help on using option -f
Reviewed-by: jfehrle
Ack-by: herbelin
|
|
|
|
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
|
|
|
|
Ack-by: Zimmi48
Reviewed-by: anton-trunov
|
|
Added user overlay for bignums
|
|
Reviewed-by: mattam82
Ack-by: ppedrot
|
|
Reviewed-by: SkySkimmer
|
|
|
|
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
|
|
Reviewed-by: jfehrle
|
|
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`.
|
|
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
|
|
Fix #7015
|
|
|
|
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.)
|
|
|
|
Reviewed-by: anton-trunov
|
|
Reviewed-by: anton-trunov
|
|
Reviewed-by: erikmd
Reviewed-by: herbelin
|
|
Reviewed-by: herbelin
Reviewed-by: maximedenes
|
|
Co-authored-by: Anton Trunov <anton.a.trunov@gmail.com>
|
|
|
|
Reviewed-by: Zimmi48
Ack-by: herbelin
Reviewed-by: ppedrot
|
|
Reviewed-by: CohenCyril
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: maximedenes
Ack-by: ppedrot
|
|
|
|
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
|
|
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>
|
|
|
|
|
