| Age | Commit message (Collapse) | Author |
|---|
|
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
|
|
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>
|
|
|
|
|
|
Reviewed-by: Lysxia
|
|
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
|
|
|
|
|
|
|
|
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
|
|
qualid in tactic notations
Reviewed-by: Zimmi48
Ack-by: jfehrle
|
|
|
|
|
|
Reviewed-by: jfehrle
|
|
n-ary applications used with applied references
Reviewed-by: ejgallego
|
|
|
|
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
|
|
Reviewed-by: ejgallego
Reviewed-by: gares
|
|
|
