| Age | Commit message (Collapse) | Author |
|---|
|
This allows to give access to all printing options (e.g. a scope or
being-in-context) to every printer w/o increasing the numbers of
functions.
|
|
We also remove trailing whitespace.
Script used:
```bash
for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done
```
|
|
Beware of 0. = -0. issue for primitive floats
The IEEE 754 declares that 0. and -0. are treated equal but we cannot
say that this is true with Leibniz equality.
Therefore we must patch the equality and the total comparison inside the
kernel to prevent inconsistency.
|
|
AFAICT the reasoning for introducing this function doesn't hold
anymore. This is needed for future refactorings that should make some
types private.
|
|
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
It will take a bit more to clean up the mess with entries in the
`indfun` plugin [quite a few PRs in the queue], but thanks to recent
refactoring the tricky parts are self-contained now in `gen_principle`
so we can remove the duplicated `save` function from the public API.
|
|
proof data on top of declare.
Reviewed-by: ppedrot
|
|
Non-delayed entries can be done with the current constructor, delayed
ones will require more work.
|
|
top of declare.
This PR is a follow up to #10406 , moving the then introduced
`proof_entry` type to `Declare`.
This makes sense as `Declare` is the main consumer of the entry type,
and already provides the constructors for it.
This is a step towards making the entry type private, which will allow
us to enforce / handle invariants on entry data better.
A side-effect of this PR is that now `Proof_global` does depend on
`Declare`, not the other way around, but that makes sense given that
closing an interactive proof will be a client of declare.
Indeed, all `Declare` / `Pfedit` / and `Proof_global` are tied into
tactics due to `abstract`, at some point we may be able to unify all
them into a single file in `vernac`.
|
|
We replace some uses of `raise (UserError ...)` with
`CErrors.user_err`, ideally we would like to make the error raising
API not depend on the exception themselves, but that's still a long
way to go.
We also rename the `Timeout` exception as to clarify purpose in the
codebase, given that it has 3 different ones as of today.
cc: #7560
|
|
Reviewed-by: ppedrot
|
|
We remove calls of `Lemmas.Info.make` that where using the default
parameters, as this is mostly dead code now.
This brings into question quite a few things, in particular, the
uneven support of `scope` attributes by different commands / plugins.
We don't attempt to solve that yet, hopefully the ongoing constant
saving path refactoring will be able to take care of these
inconsistencies.
|
|
We move `binder_kind` to the pretyping AST, removing the last data
type in the now orphaned file `Decl_kinds`.
This seems a better fit, as this data is not relevant to the lower
layers but only used in `Impargs`.
We also move state keeping to `Impargs`, so now implicit declaration
must include the type. We also remove a duplicated function.
|
|
We place control attributes on their own, datatype, similarly to
regular attributes.
This is a step towards fixing #10452 , as we can now decouple control
attributes from the vernac AST itself, allowing to pass them
independently.
|
|
|
|
|
|
This removes the export of two internal functions, moving to their
only use place.
In particular, `make_scheme` was exposing the low-level `proof_entry`
object, which should not do.
This will allow to refactor all these constant-building functions
towards a more uniform use of the API. In particular, all the
functions manipulating proof entries directly are in `Gen_principle`.
|
|
|
|
|
|
We also attempt a version that may work with `Proofview.tactic` , may
need more work.
|
|
|
|
|
|
|
|
Pointed out by Gaëtan Gilbert.
|
|
We continue over the previous commit and remove redundant
`structured_fixpoint_expr` record in favor of the one used in the AST.
This removes some term-shuffling, tho we still have discrepancies
related to adjustments on the recursive annotation.
|
|
We turn the tuples used for (co)-fixpoints into records, cleaning up
their users.
More cleanup is be possible, in particular a few functions can now
shared among co and fixpoints, also `structured_fixpoint_expr` could
like be folded into the new record.
Feedback on the naming of the records fields is welcome.
This is a step towards cleaning up code in `funind`, as it is the main
consumer of this data structure, as it does quite a bit of fixpoint
manipulation.
cc: #6019
|
|
|
|
Reviewed-by: SkySkimmer
Ack-by: ppedrot
|
|
The current code does some "opacification" for `Let`s, however that's
pretty fragile in general and not all codepaths do respect it.
We need to decide what to do.
|
|
Not pretty, but it had to be done some day, as `Globnames` seems to be
on the way out.
I have taken the opportunity to reduce the number of `open` in the
codebase.
The qualified style would indeed allow us to use a bit nicer names
`GlobRef.Inductive` instead of `IndRef`, etc... once we have the
tooling to do large-scale refactoring that could be tried.
|
|
We remove the special error printing pre-processing in favor of just
calling the standard printers.
Error printing has been a bit complex for a while due to an incomplete
migration to a new printing scheme based on registering exception
printers; this PR should alleviate that by completing the registration
approach.
After this cleanup, it should not be ever necessary for normal
functions to worry a lot about catching errors and re-raising them,
unless they have some very special needs.
This change also allows to consolidate the `explainErr` and `himsg`
modules into one, removing the need to export the error printing
functions. Ideally we would make the contents of `himsg` more
localized, but this can be done in a gradual way.
|
|
|
|
The object was mostly for wrangling universes, but we already have the
universe object for that.
It's also used by some code which iterates over objects to find
variables.
Search used to do this but was changed in a previous commit.
Prettyp.print_context and derivatives do this and I don't understand
it enough to fix it, so I kept a dummy object around. It seems like a
not very common used Print family (not documented AFAICT) so maybe we
should remove it all instead.
|
|
We can use logical kind for the same purpose, which is mainly
dumpglob, so `goal_object_kind` was never matched against, making this
transformation safe.
|
|
We remove two flags that were seldom used in favor of named parameters.
|
|
They are clearly not at the same importance level, thus we use a named
parameter and isolate the kinds as to allow further improvements and
refactoring.
|
|
We move the bulk of `Decl_kinds` to a better place [namely
`interp/decls`] and refactor the use of this information quite a bit.
The information seems to be used almost only for `Dumpglob`, so it
certainly should end there to achieve a cleaner core.
Note the previous commits, as well as the annotations regarding the
dubious use of the "variable" data managed by the `Decls` file.
IMO this needs more work, but this should be a good start.
|
|
Ack-by: ejgallego
Reviewed-by: ppedrot
|
|
We move special vernac-qed handling to a special function, making the
regular vernacular interpretation path uniform.
This is an important step as it paves the way up to export the vernac
DSL to clients, as there are no special vernacs anymore in the regular
interp path, except for Load, which should be handled separately due
to silly reasons, as morally it is a `VtNoProof` command.
|
|
We turn the hook parameter into a record, making more explicit the
capture of data in hooks as they only take one parameter now
This is a fine-tuning but provides some small advantages, and allows
us to tweak the hook type with less breakage.
|
|
|
|
This seems like the right location, a bit more refactoring should be
possible.
|
|
This is more in-line with attributes and the rest of the API, and
makes some code significantly clearer (as in `foo true false false`,
etc...)
|
|
This datatype does belong to this layer.
|
|
We split `{goal,declaration,assumption}_kind` into their
components. This makes sense as each part of this triple is handled by
a different layer, namely:
- `polymorphic` status: necessary for the lower engine layers;
- `locality`: only used in `vernac` top-level constants
- `kind`: merely used for cosmetic purposes [could indeed be removed /
pushed upwards]
We also profit from this refactoring to add some named parameters to
the top-level definition API which is quite parameter-hungry.
More refactoring is possible and will come in further commits, in
particular this is a step towards unifying the definition / lemma save path.
|
|
This information is already present on `Proof.t`, so we extract it
form there.
Moreover, this information is essential to the lower-level proof, as
opposed to the "kind" information which is only relevant to the vernac
layer; we will move it thus to its proper layer in subsequent commits.
|
|
Lemmas.info was a bit out of hand, as well as the parameters to the
`start_*` family. Most of the info is not needed and should hopefully
remain constrained to special cases, most callers only set the hook,
and obligations should be better served by a `start_obligation`
function soon.
|
|
This allows to desynchronize the kernel-facing API from the proof-facing one.
|
|
obligation ones.
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: ppedrot
|
