| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
| |
This field used to signal that a constant was the compatibility
eta-expansion of a primitive projections, but since a previous cleanup in
the kernel it had become useless.
|
| |
|
|
|
| |
Although the fix is not a proper one, it seems to solve
every instance of #2800 that could be tested.
|
| |
|
|
| |
We move the last 3 types to more adequate places.
|
| |
|
|
|
| |
This gets `Tactypes` closer to `tactics/`, however some legacy stuff
blocks it in `proofs`. We consider that is satisfactory for now.
|
| |
|
|
|
| |
- move_location to proofs/logic.
- intro_pattern_naming to Namegen.
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
| |
We add .mli files, removed dead code and use standard combinators
instead of redefined ad-hoc ones in a few places.
A lot of cleaning still has to be done on this code: documenting the
interfaces, resolving the many abstraction leaks. I suspect there is
still a lot of code duplication.
|
| |
|
|
|
| |
When called by auto, `simple apply` still does not respect `Opaque`
because of compatibility issues.
|
| |\ |
|
| |\ \ |
|
| |\ \ \ |
|
| | |_|/
|/| | |
|
| |\ \ \ |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
Previously to this patch, `Notation_term` contained information about
both parsing and notation interpretation.
We split notation grammar to a file `parsing/notation_gram` as to make
`interp/` not to depend on some parsing structures such as entries.
|
| | |_|/
|/| |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
Continuing the interface cleanup we place `Constrexpr` in the
internalization module, which is the one that eliminates it.
This slims down `pretyping` considerably, including removing the
`Univdecls` module which existed only due to bad dependency ordering
in the first place. Thanks to @ Skyskimmer we also remove a duplicate
`univ_decl` definition among `Misctypes` and `UState`.
This is mostly a proof of concept yet as it depends on quite a few
patches of the tree. For sure some tweaks will be necessary, but it
should be good for review now.
IMO the tree is now in a state where we can could easy eliminate more
than 10 modules without any impact, IMHO this is a net saving API-wise
and would help people to understand the structure of the code better.
|
| | | |
| | |
| | |
| | |
| | | |
Instead of having the projection data in the constant data we have it
independently in the environment.
|
| |/ /
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
We remove most of what was deprecated in `Term`. Now, `intf` and
`kernel` are almost deprecation-free, tho I am not very convinced
about the whole `Term -> Constr` renaming but I'm afraid there is no
way back.
Inconsistencies with the constructor policy (see #6440) remain along
the code-base and I'm afraid I don't see a plan to reconcile them.
The `Sorts` deprecation is hard to finalize, opening `Sorts` is not a
good idea as someone added a `List` module inside it.
|
| |\ \ |
|
| |\ \ \ |
|
| |\ \ \ \ |
|
| | |/ / /
|/| | |
| | | |
| | | |
| | | | |
In locally nameless mode (proof mode) names in the context *must*
be distinct otherwise the term representation makes no sense.
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
We now have only two notions of environments in the kernel: env and
safe_env.
|
| |\ \ \ \
| |/ / /
|/| | | |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
We make the vernacular implementation self-contained in the `vernac/`
directory. To this extent we relocate the parser, printer, and AST to
the `vernac/` directory, and move a couple of hint-related types to
`Hints`, where they do indeed belong.
IMO this makes the code easier to understand, and provides a better
modularity of the codebase as now all things under `tactics` have 0
knowledge about vernaculars.
The vernacular extension machinery has also been moved to `vernac/`,
this will help when #6171 [proof state cleanup] is completed along
with a stronger typing for vernacular interpretation that can
distinguish different types of effects vernacular commands can perform.
This PR introduces some very minor source-level incompatibilities due
to a different module layering [thus deprecating is not
possible]. Impact should be relatively minor.
|
| | |/ /
|/| | |
|
| |\ \ \
| | | |
| | | | |
Simplify the newring hack
|
| |\ \ \ \ |
|
| | |_|/ /
|/| | |
| | | |
| | | | |
We address the easy ones, but they should probably be all removed.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
We remove the `fix N / cofix N` forms from the tactic language. This
way, these tactics don't depend anymore on the proof context, in
particular on the proof name, which seems like a fragile practice.
Apart from the concerns wrt maintenability of proof scripts, this also
helps making the "proof state" functional; as we don't have to
propagate the proof name to the tactic layer.
|
| |\ \ \ \
| | | | |
| | | | |
| | | | | |
in CArray
|
| | | | | | |
|
| | | | | | |
|
| | | | | | |
|
| |/ / / /
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
`Proof_global` is the main consumer of the flag, which doesn't seem to
belong to the AST as plugins show.
This will allow the vernac AST to be placed in `vernac` indeed.
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
The new implementation is 100% compatible with the previous one, but it
is more compact and does not use a tricky translation function from the
kernel.
|
| | |/ /
|/| | |
|
| |\ \ \ |
|
| | |/ /
|/| | |
|
| |\ \ \ |
|
| | | | | |
|
| | | | |
| | | |
| | | |
| | | | |
Uses internal to Refiner remain.
|
| | | | | |
|
| | | | | |
|
| | |/ /
|/| |
| | |
| | | |
clear_hyps remain with no alternative
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
In #6092, `global_reference` was moved to `kernel`. It makes sense to
go further and use the current kernel style for names.
This has a good effect on the dependency graph, as some core modules
don't depend on library anymore.
A question about providing equality for the GloRef module remains, as
there are two different notions of equality for constants. In that
sense, `KerPair` seems suspicious and at some point it should be
looked at.
|
| |\ \ \ |
|
| | | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | |
| | | | |
`Vernacexpr` lives conceptually higher than `proof`, however,
datatypes for bullets and goal selectors are in `Vernacexpr`.
In particular, we move:
- `proof_bullet`: to `Proof_bullet`
- `goal_selector`: to a new file `Goal_select`
|
| |\ \ \ \ |
|
Pierre-Marie Pédrot
Cyprien Mangin
Emilio Jesus Gallego Arias
Maxime Dénès
Hugo Herbelin
Matthieu Sozeau
Armaël Guéneau
Gaëtan Gilbert
Enrico Tassi
Assia Mahboubi