| Age | Commit message (Collapse) | Author |
|---|
|
Error happened only when writing:
functional induction f x y z.
instead of
functional induction (f x y z).
Now the former is equivalent to the former: implicits must be omitted.
Hence small source of incompatibility, but a more homogeneous
behaviour.
|
|
Reviewed-by: Matafou
Ack-by: SkySkimmer
Reviewed-by: gares
|
|
Reviewed-by: ejgallego
|
|
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.
|
|
Reviewed-by: Matafou
Reviewed-by: SkySkimmer
|
|
Ack-by: Zimmi48
Reviewed-by: ppedrot
|
|
The API in `DeclareDef` should become the recommended API in `Declare`.
This greatly reduces the exposure of internals; we still have a large
offender in `Lemmas` but that will be taken care of in the next
commit; effectively removing quite some chunks from `declare.mli`.
This PR originally introduced a dependency cycle due to:
- `Declare`: uses `Vernacexpr.decl_notation list`
- `Vernacexpr`: uses `ComHint.hint_expr`
- `ComHint`: uses `Declare.declare_constant`
This is a real cycle in the sense that `ComHint` would have also move
to `DeclareDef` in the medium term.
There were quite a few ways to solve it, we have chosen to
move the hints ast to `Vernacexpr` as it is not very invasive
and seems consistent with the current style.
Alternatives, which could be considered at a later stage are for
example moving the notations AST to `Metasyntax`, having `Declare` not
to depend on `Vernacexpr` [which seems actually a good thing to do in
the medium term], reworking notation support more deeply...
|
|
|
|
|
|
Reviewed-by: Matafou
Reviewed-by: SkySkimmer
Reviewed-by: ppedrot
|
|
We will remove this modules and submit the overlays once the
refactoring is done as to avoid churn.
|
|
This is needed to make this low-level entry structures privates;
moreover, the code seems much clearer using the higher-level API.
Some more cleanup needs to be done but this is clearly a step forward
IMHO.
|
|
|
|
This function was used almost everywhere with the wrapper around.
|
|
|
|
(incidentally fixes #7697)
Reviewed-by: Lysxia
|
|
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.
|
|
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.
|
|
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?
|
|
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`.
|
|
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.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
Ack-by: SkySkimmer
Reviewed-by: jfehrle
Reviewed-by: ppedrot
|
|
Reviewed-by: Matafou
|
|
Most of the parameters were named, we fix the remaining cases.
|
|
- Legacy attributes can now be specified in any order.
- Legacy attribute Cumulative maps to universes(cumulative).
- Legacy attribute NonCumulative maps to universes(noncumulative).
- Legacy attribute Private maps to private(matching).
We use "private(matching)" and not "private(match)" because we cannot
use keywords within attributes.
|
|
Add headers to a few files which were missing them.
|
|
Fixes #11846: Funind fails to generate principles for terms with let bindings.
|
|
|
|
|
|
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`.
|
|
Reviewed-by: Zimmi48
Reviewed-by: maximedenes
Reviewed-by: ppedrot
|
|
Reviewed-by: Zimmi48
|
|
to control uniform parameters.
This replaces the attribute.
|
|
Currently, `.v` under the `Coq.` prefix are found in both `theories`
and `plugins`. Usually these two directories are merged by special
loadpath code that allows double-binding of the prefix.
This adds some complexity to the build and loadpath system; and in
particular, it prevents from handling the `Coq.*` prefix in the
simple, `-R theories Coq` standard way.
We thus move all `.v` files to theories, leaving `plugins` as an
OCaml-only directory, and modify accordingly the loadpath / build
infrastructure.
Note that in general `plugins/foo/Foo.v` was not self-contained, in
the sense that it depended on files in `theories` and files in
`theories` depended on it; moreover, Coq saw all these files as
belonging to the same namespace so it didn't really care where they
lived.
This could also imply a performance gain as we now effectively
traverse less directories when locating a library.
See also discussion in #10003
|
|
|
|
The standard use is to repeat the option keywords in lowercase, which
is basically useless.
En passant add doc entry for Dump Arith.
|
|
|
|
This is the easy part of removing unsafe_type_of, as type_of_variable
doesn't return (or even take as argument) an evar map.
|
|
|
