| Age | Commit message (Collapse) | Author |
|---|
|
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`.
|
|
|
|
|
|
|
|
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
|
|
|
|
|
|
As the text says later:
> Hints should only be made available when the module they are defined in is imported, not just required.
|
|
|
|
|
|
Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot
Ack-by: proux01
Ack-by: silene
|
|
Persistent arrays expose a functional interface but are implemented
using an imperative data structure. The OCaml implementation is based on
Jean-Christophe Filliâtre's.
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
Reviewed-by: MSoegtropIMC
Reviewed-by: gares
|
|
Reviewed-by: ppedrot
|
|
|
|
Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: maximedenes
|
|
patterns.
Reviewed-by: SkySkimmer
Reviewed-by: maximedenes
|
|
|
|
|
|
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
|
|
|
|
We unify information about constants so it is shared among all the
paths [interactive, NI, obligations].
IMHO the current setup looks pretty good, with information split into
a per-constant record `CInfo.t` and variables affecting mutual
definitions at once, which live in `Info.t`.
Main information outside our `Info` record is `opaque`, which is
provided at different moments in several cases.
There are a few nits regarding interactive proofs, which will go away
in the next commits.
|
|
This is in preparation for the next commit which will clean-up the
current API flow in `Declare`.
|
|
|
|
This improves the interface, and allows even more sealing of the API.
This is yet work in progress.
|
|
At this point the record in lemmas was just a stub; next commit will
stop exposing the internals of mutual information, and pave the way
for the refactoring of `Info.t` handling in the Declare interface.
|
|
|
|
Fixes #12582
The previous code said that `Nat.v.log` (and therefore `Nat.vo`) should
be rebuilt anytime `Nat.v.log` is older than `plik.v.vo`, and also says
that `plik.v.log` (and therefore `plik.vo`) should be rebuilt anytime
`plik.v.log` is older than `Nat.vo`. This is circular, and results in
`make` considering all of the `modules/` tests out-of-date on any fresh
run.
|
|
Fixes #12571.
|
|
Reviewed-by: MSoegtropIMC
Ack-by: SkySkimmer
|
|
Reviewed-by: fajb
|
|
|
|
Fixes #12545.
|
|
|
|
|
|
Hope this is enough, also looking at
https://github.com/coq/coq/commit/4c9ba141f8f7e067f274cb5a02293e8e52f89487#diff-a907eea979c6d310cb6208180b556d6d.
|
|
Add Zify <X> are documented.
Add <X> is deprecated as it clashed with the standard Add command
|
|
The syntax of formulae is extended to support boolean constants (true,
false), boolean operators Bool.andb, Bool.orb, Bool.implb, Bool.negb,
Bool.eqb and comparison operators Z.eqb, Z.ltb, Z.gtb, Z.leb and
Z.ltb.
|
