| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Reviewed-by: maximedenes
|
|
This still needs API cleanup but we defer it to the moment we are
ready to make the internals private.
|
|
If we remove all the legacy proof engine stuff, that would remove the
need for the view on proof almost entirely.
|
|
We place creation and saving of interactive proofs in the same module;
this will allow to make `proof_entry` private, improving invariants
and control over clients, and to reduce the API [for example next
commit will move abstract declaration into this module, removing the
exported ad-hoc `build_constant_by_tactic`]
Next step will be to unify all the common code in the interactive /
non-interactive case; but we need to tweak the handling of obligations
first.
|
|
|
|
|
|
This completes a pure Dune bootstrap of Coq.
There is still the question if we should modify `coqdep` so it does
output a dependency on `Init.Prelude.vo` in certain cases.
TODO: We still double-add `theories` and `plugins` [in coqinit and in
Dune], this should be easy to clean up.
Setting `libs_init_load_path` does give a correct build indeed;
however we still must call this for compatibility?
|
|
This corresponds more naturally to the use we make of them, as we don't need
fast indexation but we instead keep pushing terms on top of them.
|
|
|
|
|
|
|
|
If we need more fine-tuning we should manage the warnings with the
standard Coq mechanism.
|
|
There is not need to re-export Gramlib's API in a non-structured way
anymore. We thus expose the core Gramlib interface to users and remove
redundant functions.
A question about whether to move more parts of the API to `Gramlib` is
still open, as well as on naming.
|
|
We remove Coq's wrapper over gramlib's grammar constructors.
|
|
After the gramlib merge and the type-safe interface added to it, the
grammar extension type is redundant; we thus make it private as a
first step on consolidating it with the one in gramlib's.
|
|
After the gramlib merge and the type-safe interface added to it, the
grammar extension type is redundant; we thus make it private as a
first step on consolidating it with the one in gramlib's.
|
|
That is, it contains the type of the binder so as not to rely on the relevance
explicitly.
|
|
For robustness and it is better to leave it opaque. Users are not supposed to
fiddle with it.
|
|
Add headers to a few files which were missing them.
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
This fixes #11547 ; note that it is hard to register such handlers in
the `Summary` due to layering issues; there are potential anomalies here
depending on how plugins do register their data structures.
|
|
We make the primitives for backtrace-enriched exceptions canonical in
the `Exninfo` module, deprecating all other aliases.
At some point dependencies between `CErrors` and `Exninfo` were a bit
complex, after recent clean-ups the roles seem much clearer so we can
have a single place for `iraise` and `capture`.
|
|
|
|
|
|
|
|
They were in Ltac2, but they are of general interest
|
|
option
Reviewed-by: ppedrot
|
|
argument
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: tchajed
|
|
This was redundant with `iraise`; exceptions in the logic monad now
are forced to attach `info` to `Proofview.NonLogical.raise`
|
|
Raising inside exception printers is quite tricky as the order of
registration for printers will indeed depend on the linking order.
We thus forbid this, and make our API closer to the upstream
`Printexn` by having printers return an option type.
|
|
This PR is in preparation of #9067 (together with #11647) .
Before this PR, `grammar_extend` always took an optional `reinit`
argument, even if it was never set to `Some ...`. Indeed, there is a
single case where reinit is needed; we track it now by using a
different extension rule constructor.
|
|
We use the same kind of trick as the one we used for &IDENT, namely check
that no space appear between the dollar sign and the identifier.
|
|
Actually, callers of the Pvernac.register_proof_mode function have to
manually register the parsing of vernacular queries themselves. This
probably qualifies as an oversight from myself.
|
|
This prevents some warnings to be dropped when the variables are not used at
the right type. See #11603 for a motivation.
|
|
The standard use is to repeat the option keywords in lowercase, which
is basically useless.
En passant add doc entry for Dump Arith.
|
|
Reviewed-by: SkySkimmer
|
|
|
|
There was an evar leak due to an evarmap not being threaded correctly
when computing open terms.
|
|
|
|
a module
Reviewed-by: ppedrot
|
|
|
|
|
|
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: maximedenes
Ack-by: proux01
Ack-by: silene
Ack-by: vbgl
|
|
|
|
|
