diff options
| author | Emilio Jesus Gallego Arias | 2019-06-10 23:11:06 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-09-18 16:16:00 +0200 |
| commit | 42ff3109217452853c3b853d21f09a317dd6e37d (patch) | |
| tree | d95cc4e262956c48fe15b02ce59c6507420b305b /dev | |
| parent | c5ecc185ccb804e02ef78012fc6ae38c092cc80a (diff) | |
[library] Move `Declaremods` to `vernac/`
We move `Declaremods` to the vernac layer as it implement
vernac-specific logic to manipulate modules which moreover is highly
imperative.
This forces code [such as printing] to manipulate the _global
imperative_ state which is a bit fishy.
The key improvement in this PR is that now `Global` is not used
anymore in `library`, so we can proceed to move it upwards.
This move is a follow-up of #10562 and a step towards moving `Global`
upper, likely to `interp` in the short term.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions