| Commit message (Collapse) | Author | Age |
|
|
|
|
|
| |
This reduces conversions between ContextSet/UContext and encodes
whether we are polymorphic by which constructor we use rather than
using some boolean.
|
|
|
|
|
|
| |
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 dont care about the order of the binder map ([map] in the code) so
no need to do tricky things with it.
|
| |
|
| |
|
| |
|
| |
|
|
Currently, the STM, vernac interpretation, and the toplevel are
intertwined in a mutual dependency that needs to be resolved using
imperative callbacks.
This is problematic for a few reasons, in particular it makes the
interpretation of commands that affect the document quite intricate.
As a first step, we split the `toplevel/` directory into two: "pure"
vernac interpretation is moved to the `vernac/` directory, on which
the STM relies.
Test suite passes, and only one command seems to be disabled with this
approach, "Show Script" which is to my understanding
obsolete. Subsequent commits will fix this and refine some of the
invariants that are not needed anymore.
|