| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Rewriter needs a bit of work as it calls a removed function, but no
big deal.
|
|
This still needs API cleanup but we defer it to the moment we are
ready to make the internals private.
|
|
This makes the API more orthogonal and allows better structure in
future code.
|
|
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: Zimmi48
Reviewed-by: jfehrle
Reviewed-by: maximedenes
Ack-by: ppedrot
|
|
|
|
NB: 3 dots doesn't play well with PG's sentence detection.
|
|
|
|
|
|
|
|
We factorize code from declareInd.ml and inductiveops.ml which was
already existing in record.ml.
We keep expansion of local definitions in the type of fields of
primitive records while these are not expanded in the non-primitive
case. This is to be consistent with what Indtypes.compute_projections
is doing. See discussion at #11135.
We keep the unused code from inductiveops.ml for possible future use
though.
Include improvements contributed by Gaëtan Gilbert.
|
|
|
|
We deprecate `Hide Obligations` and remove `Shrink Obligations`
[deprecated since 8.7]
|
|
definitions.
Reviewed-by: SkySkimmer
|
|
Let vs Definition / Example syntax was split in 7c28130 for parsing
reasons: so that the new Let Fixpoint and Let CoFixpoint syntax could
be introduced. This split is probably the reason why Let was
overlooked when support for universe bindings and universe constraints
were added to Definition and variants.
|
|
- 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.
|
|
The location was missing in the parser.
|
|
This was an undocumented equivalent of the Section command.
|
|
Ack-by: SkySkimmer
Reviewed-by: maximedenes
|
|
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
arguments
Ack-by: SkySkimmer
Ack-by: gares
Reviewed-by: herbelin
|
|
|
|
|
|
Co-authored-by: Jasper Hugunin <jasper@hugunin.net>
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
Following an observation by Enrico Tassi, we remove the `opaque`
parameter from `close_future_proof`, it should never be called with
transparent constants.
We will enforce this thru typing at the proof layer soon.
|
|
This is a small refactoring as these two functions behave very
differently and the invariants are quite different, in fact regular
`return_proof` should not be exported but be part of close proof, but
there is small use in the STM still.
|
|
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.
|
|
Ack-by: Matafou
Reviewed-by: SkySkimmer
|
|
grammar.
Reviewed-by: ejgallego
Reviewed-by: maximedenes
|
|
Suggested by Gaëtan Gilbert.
|
|
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`.
|
|
`wits` is actually not used, it is set in equations to the list of
evars corresponding to the goals.
|
|
|
|
|
|
|
|
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 was introduced in #6203 , but as far as I can see this
re-normalization step is not necessary.
|
|
`sigma` here is actually created from `uctx`, we also uniformize
naming.
|
|
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
|
|
We don't the parameter anymore as the paths are too different now.
Note that this removes a duplicate `check_evars` that has been in
`master` quite some time [double check in `ComDefinition` and in
`DeclareDef.prepare_definition`]
|
|
Preparation of obligation/program entries requires low-level
manipulation that does break the abstraction over `proof_entry`; we
thus introduce `prepare_obligation`, and move the code that prepares
the obligation entry to its own module.
This seems to improve separation of concerns, and helps clarify the
two of three current models in which Coq operates w.r.t. definitions:
- single, ground entries with possibly mutual definitions [regular lemmas]
- single, non-ground entries with possibly mutual definitions [obligations]
- multiple entries [equations]
|
|
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.
|
|
This is a tiny step towards making the code closer to its counterpart
in `DeclareDef`.
|
|
In previous versions of Coq `abstract` could create non-uniform bodies
for mutually recursive definitions (c.f. bug #5065)
Thanks to changes to the trusted base this is not the case anymore,
thus we can remove the workaround.
This way mutual bodies are handled the same in the interactive and
non-interactive case.
|
|
|
|
This gets us closer to the code in `DeclareDef` for the
non-interactive case.
|
|
After the refactorings proof information is organized in a slightly
different way thus the lower layers don't need to pass info back
anymore.
|
