| Age | Commit message (Collapse) | Author |
|---|
|
|
|
We ungroup the rewrite scheme-defined constants, while only exporting a
function to turn the last added constant into a private constant.
|
|
This is an experimental PR as I am not sure I can follow the reasoning
in e1ba72037191b1d4be9de8a0a8fc1faa24eeb12c
Note that in safe_typing we avoid re-declaring effects twice.
This removes a huge number of redeclaration of schemes side-effects
that in fact are already generated such as `eq_ind`.
Anyways we should deprecate the declaration of Schemes on-the-fly, I
don't see the point honestly; just make sure your theory has the right
ones.
Well, going to a more eager declaration scheme could be costly in
terms of size, so OMMV.
TODO: only declare side-effects if the scheme is generated on-the-fly,
add a parameter to the declaration function.
|
|
I think the usage looks cleaner this way.
|
|
|
|
|
|
We remove sections paths from kernel names. This is a cleanup as most of the times this information was unused. This implies a change in the Kernel API and small user visible changes with regards to tactic qualification. In particular, the removal of "global discharge" implies a large cleanup of code.
Additionally, the change implies that some machinery in `library` and `safe_typing` must now take an `~in_section` parameter, as to provide the information whether a section is open or not.
|
|
We simply exploit a type isomorphism to remove the use of dedicated algebraic
types in the kernel which are actually not necessary.
|
|
|
|
|
|
Should it be removed? The underlying
`universe_subst -> constr -> constr`
seems like it could be useful for plugins but where would the
substitution be from?
|
|
UState normalize -> minimize, Evd nf_constraints -> minimize_universes
|
|
|
|
|
|
This code was not used at all inside the kernel, it was related to universe
unification that happens in the upper layer. It makes more sense to put it
somewhere upper.
|
|
Also use constant_universes_entry instead of a bool flag to indicate
polymorphism in ParameterEntry.
There are a few places where we convert back to ContextSet because
check_univ_decl returns a UContext, this could be improved.
|
|
We can enforce properties through check_univ_decl, or get an arbitrary
ordered context with UState.context / Evd.to_universe_context (the
later being a new wrapper of the former).
|
|
We do up to `Term` which is the main bulk of the changes.
|
|
This will allow to merge back `Names` with `API.Names`
|
|
We use an algebraic type instead of a pair of a boolean and the corresponding
data. For now, this is isomorphic, but this allows later change in the structure.
|
|
We move a bunch of modules (`Impargs`, `Declare`, `Ind_tables`,
`Miscprint`) to their proper place as they were declared in different
`mllib` files than the one in their directory.
In some cases this could be refined but we don't do anything fancy, we
just reflect the status quo.
|
