| Age | Commit message (Collapse) | Author |
|---|
|
It makes sense to require it to be uni-goal; this also removes some
duplication.
See the caveat with the handling of `~sign` tho.
|
|
This should make the univbinders output test less fragile as it
depends less on the global counter (still used for universes from
section variables).
|
|
Reviewed-by: SkySkimmer
|
|
|
|
This will ensure that we don't introduce problems as it has happened
in the past.
While we are at it, we fix one easy case of non-tail call.
|
|
In the current proof save path, the kernel can raise an exception when
checking a proof wrapped into a future.
However, in this case, the future itself will "fix" the produced
exception, with the mandatory handler set at the future's creation
time.
Thus, there is no need for the declare layer to mess with exceptions
anymore, if my logic is correct. Note that the `fix_exn` parameter to
the `Declare` API was not used anymore.
This undoes 77cf18eb844b45776b2ec67be9f71e8dd4ca002c which comes from
pre-github times, so unfortunately I didn't have access to the
discussion.
We need to be careful in `perform_buildp` as to catch the `Qed` error
and properly notify the STM about it with `State.exn_on`; this was
previously done by the declare layer using a hack [grabbing internal
state of the future, that the future itself was not using as it was
already forced], but we now do it in the caller in a more principled
way.
This has been tested in the case that tactics succeed but Qed fails
asynchronously.
|
|
Reviewed-by: ejgallego
|
|
Fix #12447
|
|
Fixes #12390
|
|
In particular this avoids exposing `Evd.side_effects proof_entry` in
the API.
|
|
deprecation.
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
|
|
Reviewed-by: SkySkimmer
|
|
|
|
This complements #11407 about storing digests of modules.
|
|
A step towards enforcing some more static invariants.
|
|
|
|
A step towards enforcing some more static invariants.
|
|
A step towards enforcing some more static invariants.
|
|
|
|
This is not needed outside of `Declare` now.
|
|
|
|
|
|
This reduces the amount of exported internals, in particular
w.r.t. proof delaying and side effects which we will need in future
refactorings.
Actually turning the type from `Evd.side_effects proof_entry` to `unit
proof_entry` is left for the next commits.
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: JasonGross
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
|
|
|
|
This removes a use of internal obligation data `prg_poly` and a couple
of duplicate lines.
|
|
|
|
Not necessary anymore after the merge of obligation declaration into
the main path.
|
|
Reviewed-by: SkySkimmer
|
|
Closes #12351.
We set the parameters of the redirect formatter to be same than the
ones in stdout.
I guess the original semantics was to ignore the parameters, so I'm
unsure we want to do this.
While we are a it, we include a fix on the formatter, which _must_ be
flushed before closing its associated channel.
|
|
|
|
|
|
|
|
This seems like a recurring pattern, and IMO makes a bit better API.
We also remove `merge_universe_subst` as it is not needed so far, as
we were creating stale `evar_map`s just for this purpose.
|
|
We complete some arduous refactoring in order to bring all the
internals and code of constant / proof saving into the same module.
In particular, this PR moves the remaining parts of proof saving from
`Lemmas` to `Declare`.
The reduction in exposed internals is considerable; in particular, we
remove the export of the internals of `proof_entry` and `proof_object`
[used in delayed proofs], which will allow us to start to address many
issues with the current setup, such as #10363 .
There are still some TODOs, that will be addressed in subsequent PRs:
- Remove `declare_constant` in favor of higher-level APIs
- Then, remove access to `proof_entry` entirely
- Refactor current very verbose handling of proof info.
- Remove compat modules / API.
- Rework handling of delayed proofs [this may be hard due to state and the STM]
- Reify Hook API for the case where it acts as a continuation [that is to say, declaring constants from the Hook]
List of remaining offenders for `proof_entry` / `declare_constant` in
the codebase:
- File "vernac/comHints.ml"
- File "vernac/indschemes.ml"
- File "vernac/comProgramFixpoint.ml"
- File "vernac/comAssumption.ml"
- File "vernac/record.ml"
- File "plugins/ltac/leminv.ml"
- File "plugins/setoid_ring/newring.ml"
- File "plugins/funind/recdef.ml"
- File "plugins/funind/gen_principle.ml"
|
|
This is needed as a first step to refactor and unify the obligation
save path and state; in particular `Equations` is a heavy user of
Hooks to modify obligations state, thus in order to make the hook
aware of this we need to place the obligation state before the hook.
As a good side-effect, `inline_private_constants` and `Hook.call` are
not exported from `Declare` anymore.
|
|
In our quest to unify all the declaration paths, an important step
is to account for the state pertaining to `Program` declarations.
Whereas regular proofs keep are kept in a stack-like structure;
obligations for constants defined by `Program` are stored in a global
map which is manipulated by almost regular open/close proof primitives.
This PR is in preparation for the switch to a purely functional state
in #11836 ; the full switch requires deeper changes so it is helpful
to have this PR preparing most of the structure.
Most of the PR is routine; only remarkable change is that the hook for
admitted obligations is now called explicitly in `finish_admitted` as
it had to learn about the different types of proof_endings. Before,
obligations set it in `start_lemma` but only used in the `Admitted`
path.
|
|
but ssrsearch is not loaded.
Fixes #12338
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: ejgallego
Ack-by: kyoDralliam
|
|
The main use case of SearchHead is now handled by headconcl:
The secondary use case was redundant with SearchPattern.
|
|
|
|
|
|
|
|
|
|
- new clauses "hyp:", "concl:", "headhyp:" and "headconcl:" to restrict
match to an hypothesis or the conclusion, possibly only at the head
(like SearchHead in this latter case)
- new clause "is:" to search by kind of object (for some list of kinds)
- support for any combination of negations, disjunctions and conjunctions,
using a syntax close to that of intropatterns.
|
|
|
|
Re-raising inside exception handlers must be done with care in order
to preserve backtraces; even if newer OCaml versions do a better job
in automatically spilling `%reraise` in places that matter, there is
no guarantee for that to happen.
I've done a best-effort pass of places that were re-raising
incorrectly, hopefully I got the logic right.
There is the special case of `Nametab.error_global_not_found` which is
raised many times in response to a `Not_found` error; IMHO this error
should be converted to something more specific, however the scope of
that change would be huge as to do easily...
|
|
runtime.
Reviewed-by: herbelin
|
|
Reviewed-by: SkySkimmer
|
