| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
(Universes and Evd)
|
| |
|
|
|
|
|
|
|
| |
This shall eventually allow to use contexts of declarations in the
definition of the "Case" constructor.
Basically, this means that Constr now includes Context and that the
"t" types of Context which were specialized on constr are not defined
in Constr (unfortunately using a heavy boilerplate).
|
| |\ |
|
| |\ \ |
|
| |\ \ \
| | | |
| | | |
| | | | |
constants
|
| | |_|/
|/| | |
|
| | | |
| | |
| | |
| | |
| | | |
Apparently it was not useful. I don't remember what I was thinking
when I added it.
|
| |\ \ \
| |/ /
|/| | |
|
| |\ \ \ |
|
| | | | |
| | | |
| | | |
| | | |
| | | | |
The test isn't quite the one in #7421 because that use of algebraic
universes is wrong.
|
| |/ / /
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
reference was defined as Ident or Qualid, but the qualid type already
permits empty paths. So we had effectively two representations for
unqualified names, that were not seen as equal by eq_reference.
We remove the reference type and replace its uses by qualid.
|
| | |/
|/|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
When restricting an evar with candidates, raise an exception if this
restriction would leave the evar without candidates, i.e. unsolvable.
- evarutil: mark restricted evars as "cleared"
They would otherwise escape being catched by the [advance] function
of clenv, and result in dangling evars not being registered to the shelf.
- engine: restrict_evar marks it cleared, update the future goals
We make the new evar a future goal and remove the old one.
If we did nothing, [unshelve tac] would work correctly as it
uses [Proofview.advance] to find the shelved goals, going through
the cleared evar. But [Unshelve] would fail as it expects only
undefined evars on the shelf and throws away the defined ones.
|
| |/
|
|
| |
Avoid adding the same unification problem twice, module evar instantiation.
|
| |
|
|
|
| |
- move_location to proofs/logic.
- intro_pattern_naming to Namegen.
|
| | |
|
| | |
|
| |\ |
|
| |\ \ |
|
| | | |
| | |
| | | |
Actually all the new_ functions are in evarutil still
|
| | |/
|/| |
|
| |\ \ |
|
| | | |
| | |
| | |
| | | |
Most of it seems straightforward.
|
| | |/
|/|
| |
| | |
Note that `Assumptions` ships its own copy, but for `Constr.t`.
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| | | | |
|
| | | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | |
| | | |
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.
|
| | |/
|/| |
|
| |\ \ |
|
| | | |
| | |
| | |
| | |
| | | |
We now have only two notions of environments in the kernel: env and
safe_env.
|
| |/ /
| |
| |
| | |
We address the easy ones, but they should probably be all removed.
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| | |
This finishes the splitting of Universes.
|
| | | |
|
| | | |
|
| | | |
|
| | | |
|
| | |
| |
| |
| | |
This API is a bit strange, I expect it will change at some point.
|
| | | |
|
| |\ \ |
|
| | | | |
|
| | | | |
|
| | | |
| | |
| | |
| | | |
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.
|
Gaëtan Gilbert
Hugo Herbelin
Pierre-Marie Pédrot
Gaëtan Gilbert
Enrico Tassi
Maxime Dénès
Matthieu Sozeau
Emilio Jesus Gallego Arias
Matthieu Sozeau