| Age | Commit message (Collapse) | Author |
|---|
|
This removes so ad-hoc tuples, and encapsulates the API a bit.
It is a step towards:
- Pushing some `to_constr` from the upper layers to the declare code
itself [which will remove code duplication, in particular making the
interactive / non-interactive path more uniform, and make the API
easier to use]
- Further refactoring of the constant information, as `Recthm.t`
contains almost now what we would call "primitive constant
information"; thus we will be able to distinguish next better between
mutual declarations and single-constant ones.
|
|
When declaring a lemma, the code path is quite different depending on
whether the lemma is inferred to be a mutually-defined lemma or not.
We refactor the code path in declare to reflect that; this will allow
to better organize constant information and to reuse the `Recthm.t`
type in particular.
|
|
|
|
|
|
|
|
|
|
Step towards merging `Info / `CInfo`; the presentation order is now
"final" in the sense of that we propose this API for the medium-term.
|
|
This is in preparation for the next commit which will clean-up the
current API flow in `Declare`.
|
|
|
|
|
|
The previous refactoring in `Declare` to add `CInfo.t` makes this a
good moment to clean overlays up w.r.t. deprecation.
All cases but one is just a matter of simple renaming, for the other
the use of an internal API is replaced by newer API.
|
|
This hides even more internals; we will reduce the API even more
shortly.
|
|
This improves the interface, and allows even more sealing of the API.
This is yet work in progress.
|
|
The module is now a stub. We choose to be explicit on the parameters
for now, this will improve in next commits with the refactoring of
proof / constant information.
|
|
We move the advanced proof initialization routine to Declare, and stop
exposing implementation internals in `Info.t` constructor.
|
|
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.
|
|
It makes sense to require it to be uni-goal; this also removes some
duplication.
See the caveat with the handling of `~sign` tho.
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
|
|
|
|
Ack-by: SkySkimmer
Reviewed-by: gares
|
|
This partially reverts commit 35a1cc4f5c708b745a2810a64d220f49eff4beca.
(I've not added back the nix things, since I'm not sure what purpose
they serve, and I've adjusted the targets slightly.)
The CI build should no longer take an enormously long time to start, and
fiat-crypto-legacy code is actively being used to track down memory
issues in #12487. Additionally, f-c-l revealed a genuine bug in #7825,
and so I'd like to keep f-c-l in the CI at least until #7825 is
finished.
I've been maintaining compatibility of f-c-l with master anyway on the
side, in part to continue some performance experiments with it, and
expect to continue to do so at least until the end of this calendar
year, and it'd be nice for me to get advance warning when a PR is going
to break it on master. (It seems reasonable to me to take it off the CI
again once I'm no longer maintaining it / collecting data from it, and /
or once #7825 is finished.)
|
|
They were deprecated in 8.12.
|
|
No need to return the list of generated evars, this was never used.
|
|
|
|
Having two different modules led to the availability of internal API in
the mli.
|
|
All calls to this function are now factorized through Clenvtac.res_pf.
|
|
|
|
Reviewed-by: ejgallego
Ack-by: maximedenes
|
|
Reviewed-by: mattam82
|
|
This reverts commit b35030760cadd96a968e04f3cd026f4abdc0331c.
|
|
Reviewed-by: SkySkimmer
|
|
It's tested on the bench, so might as well test it on the CI. Hopefully
it's not too memory-heavy. (It should only take a couple of minutes,
time-wise.)
|
|
Reviewed-by: MSoegtropIMC
Ack-by: SkySkimmer
|
|
Reviewed-by: gares
Reviewed-by: maximedenes
|
|
|
|
Reviewed-by: fajb
|
|
Reviewed-by: SkySkimmer
|
|
|
|
Instead of dropping the unification result and calling simple eapply with
the original term, we simply use the same code path as auto and typeclass
eauto, i.e. reuse the clenv for refinement.
|
|
Reviewed-by: herbelin
|
|
|
|
variables in goals
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: ejgallego
|
|
|
|
Reviewed-by: herbelin
|
|
Reviewed-by: jfehrle
|
|
Fixes #12545.
|
