| Age | Commit message (Collapse) | Author |
|---|
|
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
|
|
Reviewed-by: Matafou
Ack-by: SkySkimmer
Reviewed-by: gares
|
|
This seems to be a pattern used quite a bit in the wild, it does not hurt
to be a bit more lenient to tolerate this kind of use. Interestingly the
API was already offering a similar generalization in some unrelated places.
We also backtrack on the change in Floats.FloatLemmas since it is an instance
of this phenomenon.
|
|
We take the env of the current goal with the context replaced with
section variables. In practice, this is the global env, but, maybe,
one day, a goal state will have its own env.
|
|
Reviewed-by: SkySkimmer
|
|
Ack-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: mattam82
|
|
Reviewed-by: ejgallego
|
|
|
|
This makes the invariants in the code clearer, and also highlight this is
only required to implement template polymorphic inductive types.
|
|
Reviewed-by: Zimmi48
Reviewed-by: jfehrle
Ack-by: ppedrot
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
|
|
We tweak the message a bit.
|
|
|
|
They were not used anywhere anymore.
|
|
This was useless, since we did not observe the difference on evars.
|
|
Ack-by: Zimmi48
Ack-by: ejgallego
Ack-by: herbelin
Ack-by: ppedrot
|
|
This is extracted from #9710, where we need the environment anyway to compute
iota rules on inductive types with let-bindings. The commit is self-contained,
so I think it could go directly in to save me a few rebases.
Furthermore, this is also related to #11707. Assuming we split cbn from the
other reduction machine, this allows to merge the "local" machine with
the general one, since after this PR they will have the same type. One less
reduction machine should make people happy.
|
