| Age | Commit message (Collapse) | Author |
|---|
|
`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.
|
|
This could still use some more work due to the way proofs are
structured, in particular:
- the handling of the primary type w.r.t. Econstr
- refining Info.t so open/close invariants hold by typing
Very interestingly, better typing means that the tension between
tension between `start_dependent_lemma` and the handling of mutual
definitions starts to surface.
In particular, the information contained in `Info.thms` is not to be
used by all non-standard terminators.
However, it seems that such refactoring would better fit once we have
finished cleaning up the regular save path.
|
|
Ack-by: SkySkimmer
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Reviewed-by: herbelin
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
|
|
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
|
|
Fix #11967
|
|
|
|
|
|
The completion proposals need to be ordered by length first for usability.
I aknowledge that it's too easy to mess up when refactoring, but here there was
a clear comment that this change should not have been performed.
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
Reviewed-by: SkySkimmer
Reviewed-by: herbelin
Ack-by: ppedrot
|
|
Reviewed-by: SkySkimmer
|
|
|
|
Reviewed-by: Zimmi48
|
|
Ack-by: Zimmi48
Reviewed-by: anton-trunov
Ack-by: jfehrle
Reviewed-by: maximedenes
|
|
Ack-by: SkySkimmer
Reviewed-by: ejgallego
|
|
|
|
|
|
|
|
Fix makefile glitches
|
|
Reviewed-by: ejgallego
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: erikmd
|
|
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
|
|
|
|
- Removal of exported types and functions that were unused.
- Moving ad-hoc functions that were used once in the codebase to their call site.
|
|
|
|
|
|
We propose to add an environment to have foldable texts with HTML
output, more precisely:
(*begin details [: An optional summary] *)
some Coq and documentation material
(* end details *)
Currently, only the HTML output is supported. We could treat this
environment in LaTeX output as appendixes to output later.
|
|
|
|
Use `dune build @check-gram --auto-promote` to automatically update
these two files. You will need to run it twice if the two files need
to be updated (which is the case most often) as Dune will stop after
the first diff failure.
The rst files are also updated but left in the `_build/` directory as
Dune wouldn't support targets outside the current directory. You can
just `mv _build/default/doc/sphinx doc` to update them after running
the @check-gram target.
|
|
|
