| Age | Commit message (Collapse) | Author |
|---|
|
This lets us avoid passing ~ontop to do_definition and co, and after #10050
to even more functions.
|
|
|
|
Supersedes #8718.
|
|
I think the usage looks cleaner this way.
|
|
|
|
We make `declaration_hook`s optional arguments everywhere, and thus we
avoid some "fake" functions having to be passed.
This identifies positively the code really using hooks [funind,
rewrite, coercions, program, and canonicals] and helps moving toward
some hope of reification.
|
|
"Declaration" hooks can be polymorphic on their return type, however
this facility doesn't seem used in the codebase.
We thus remove the polymorphism with the hope to be able to reify the
control later on.
|
|
This API is a bit strange, I expect it will change at some point.
|
|
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.
|
|
|
|
This reduces conversions between ContextSet/UContext and encodes
whether we are polymorphic by which constructor we use rather than
using some boolean.
|
|
We do up to `Term` which is the main bulk of the changes.
|
|
This was (once again) a spurious inter-dependency, that we solve by
introducing a new module with the proper functionality. This helps in
cleaning up the code. Note that no code was changed, other than
removing the setting of the references.
|
