| Age | Commit message (Collapse) | Author |
|---|
|
We dont care about the order of the binder map ([map] in the code) so
no need to do tricky things with it.
|
|
evd: Move constrain_variables to an operation on UState
Necessary to check universe declarations correctly for deferred proofs
in particular.
|
|
Introduce a "+" modifier for universe and constraint declarations to
indicate that these can be extended in the final definition/proof. By
default [Definition f] is equivalent to [Definition f@{+|+}], i.e
universes can be introduced and constraints as well. For [f@{}] or
[f@{i j}], the constraints can be extended, no universe introduced, to
maintain compatibility with existing developments. Use [f@{i j | }] to
indicate that no constraint (nor universe) can be introduced. These
kind of definitions could benefit from asynchronous processing.
Declarations of universe binders and constraints also works for
monomorphic definitions.
|
|
|
|
Use an explicit label ~algebraic for make_flexible_variable as well.
|
|
|
|
|
|
Using dummy comment to @raise to please ocamldoc. Please change MS or
PMP, if needed.
|
|
longer stable w.r.t. equality constraints as the universe graph will
choose different canonical levels depending on the equalities given to
it (l = r vs r = l).
|
|
|
|
|
|
|
|
This allows to remove a lot of independent code from Evd which was put
into the UState module. The API is not perfect yet, but this is a first
pass. Names of data structures should be thought about too because they
are way too similar.
|
