diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-11-19 17:49:32 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-11-19 17:52:34 +0100 |
| commit | cfc0fc0075784e75783c9b4482fd3f4b858a44bf (patch) | |
| tree | c21ad8c78fc2613d51e50128525f09ed377ac6d8 /library/global.ml | |
| parent | 9d47cc0af706ed1cd4ab87c2d402a0457a9b6a5c (diff) | |
Allow program hooks to see the refined universe_context at the end of a
definition, if they manipulate structures depending on the initial state
of the context.
Diffstat (limited to 'library/global.ml')
0 files changed, 0 insertions, 0 deletions