| Age | Commit message (Collapse) | Author |
|---|
|
Note currently it's impossible to define inductives in SProp because
indtypes.ml and the pretyper aren't fully plugged.
|
|
This should give better visibility of universe specific operations vs
generic graph operations.
|
|
When making a universe a variable we iterate through the universes
we're equal to and if we find one we update the substitution
accordingly.
NB: The bug called make_flexible_variable on Top.15 and
~~~
{Top.15 Top.14} |= Top.11 < Top.6
Top.14 < Top.5
Top.11 = Top.15
ALGEBRAIC UNIVERSES:{Top.17 Top.16}
UNDEFINED UNIVERSES:Top.17 := Top.14+1
Top.16 := Top.14+1
WEAK CONSTRAINTS:
~~~
so now we would add [Top.15 := Top.11].
|
|
|
|
|
|
A few of them will be of help for future cleanups. We have spared the
stuff in `Names` due to bad organization of this module following the
split from `Term`, which really difficult things removing the
constructors.
|
|
Keep the universe_levels_of_constr function inside typeops, not
exported.
|
|
Not sure if worth using in other places.
|
|
|
|
ie don't go through having Eq constraints but directly to the unionfind.
|
|
|
|
|
|
|
|
We do up to `Term` which is the main bulk of the changes.
|
|
|
|
We export a function in UGraph to check that a polymorphic instance is
a subtype of another, instead of rolling up our own in module code.
We also add a few tests for module subtyping in presence of polymorphic
constants.
|
|
|
|
|
|
We export the relevant level equality function in UGraph which is way faster
than checking that each one is smaller than the other as universes.
|
|
1. The Univ module now only cares about definitions about universes.
2. The UGraph module contains the algorithm responsible for aciclicity.
|
