| Age | Commit message (Collapse) | Author |
|---|
|
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.
|
