| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
Porting them is still to be done, but at least we don't rely on the wrapper
everywhere.
|
|
Moving code around uncovered this bug.
|
|
|
|
This function was used almost everywhere with the wrapper around.
|
|
Reviewed-by: ppedrot
|
|
|
|
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Reviewed-by: maximedenes
|
|
This PR moves `Declare` to `vernac` which will hopefully allow to
unify it with `DeclareDef` and avoid exposing entry internals.
There are many tradeoffs to be made as interface and placement of
tactics is far from clear; I've tried to reach a minimally invasive
compromise:
- moved leminv to `ltac_plugin`; this is unused in the core codebase
and IMO for now it is the best place
- hook added for abstract; this should be cleaned up later
- hook added for scheme declaration; this should be cleaned up later
- separation of hints vernacular and "tactic" part should be also done
later, for now I've introduced a `declareUctx` module to avoid being
invasive there.
In particular this last point strongly suggest that for now, the best
place for `Class_tactics` would be also in `ltac`, but I've avoided
that for now too.
This partially supersedes #10951 for now and helps with #11492 .
|
|
This moves the vernacular part of hints to `vernac`; in particular, it
helps removing the declaration of constants as parts of the `tactic`
folder.
|
|
|
|
(incidentally fixes #7697)
Reviewed-by: Lysxia
|
|
|
|
Reviewed-by: SkySkimmer
Ack-by: herbelin
Reviewed-by: ppedrot
|
|
This provides linking, appropriate coloring and appropriate hovering
in coqdoc documents.
In particular, this fixes #7697.
|
|
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 actually gets `Pfedit` out of the dependency picture [can be
almost merged with `Proof` now, as it is what it manipulates] and
would allow to reduce the exported low-level API from `Proof_global`,
as `map_fold_proof` is not used anymore.
|
|
Reviewed-by: Matafou
Ack-by: Zimmi48
Ack-by: maximedenes
|
|
|
|
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?
|
|
Reviewed-by: ppedrot
|
|
As part of the proof refactoring work I am doing some modifications to
`funind` and indentation of that code is driving me a bit crazy; I'd
much prefer to delegate it to an automatic tool.
|
|
- Provide new helper functions in `Goptions` on the model of
`declare_bool_option_and_ref`;
- Use these helper functions in many parts of the code base
(encapsulates the corresponding references);
- Move almost all options from `declare_string_option` to
`declare_stringopt_option` (only "Warnings" continue to use the
former). This means that these options now support `Unset` to get
back to the default setting. Note that there is a naming
misalignment since `declare_int_option` is similar to
`declare_stringopt_option` and supports `Unset`. When "Warning" is
eventually migrated to support `Unset` as well, we can remove
`declare_string_option` and rename `declare_stringopt_option` to
`declare_string_option`.
- For some vernac options and flags that have an equivalent
command-line option or flag, implement it like the standard `-set`
and `-unset`.
|
|
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.
|
|
Reviewed-by: ppedrot
|
|
|
|
in favor of the one in the OCaml standard library.
|
|
arguments
Ack-by: SkySkimmer
Ack-by: gares
Reviewed-by: herbelin
|
|
Reviewed-by: Matafou
Ack-by: SkySkimmer
Reviewed-by: gares
Reviewed-by: ppedrot
|
|
|
|
Reviewed-by: Matafou
Reviewed-by: ppedrot
|
|
|
|
|
|
We make the types of the delayed / non-delayed declaration path
different, as the latter is just creating futures that are forced
right away.
TTBOMK the new code should behave identically w.r.t. old one, modulo
the equation `Future.(force (from_val x)) = x`.
There are some questions as what the code is doing, but in this PR
I've opted to keep the code 100% faithful to the original one, unless
I did a mistake.
|
|
This will allow to share the definition metadata for example with
obligations; a bit more work is needed to finally move the preparation
of interactive proofs from Proof_global to `prepare_entry`.
|
|
The only reasons that `prepare_definition` returned a sigma were:
- to obtain the universe binders to be passed to declare
- to obtain the UState.t to be passed to the equations hook
We handle this automatically now; it seems like a reasonably good API
improvement.
However, it is not clear what we do now is right for all cases; must
check.
|
|
This is a step in forcing all entry creation go thru the preparation
functions. We still need to handle plain `Declare.` calls, but this
will be next step.
We need to leave a backdoor for interactive proofs until we unify
proof preparation happening in `Proof_global` with the one happening
in `DeclareDef`, but we are getting there.
TODO: see how to avoid the normalization problems in DeclareObl
|
|
Proof "preparation" [as in `DeclareDef.prepare_definition`] is fairly
more complicated in the Program case; in particular, it includes
checking the existential variables, and elaborating a list of entries
from the holes.
Indeed, in the `Program` case we cannot use
`DeclareDef.prepare_definition` while keeping a good level of
abstraction, so we should introduce a `prepare_obligation` function.
This PR is in preparation for that.
|
|
After the refactorings proof information is organized in a slightly
different way thus the lower layers don't need to pass info back
anymore.
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
Using disable=true in .ocamlformat and disable=false in sub
.ocamlformat works fine.
Note that disable=true must be after the `profile` setting otherwise
it gets reset
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: erikmd
|
