diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-09-23 16:00:49 +0200 |
|---|---|---|
| committer |  Matthieu Sozeau <mattam@mattam.org> | 2015-10-02 15:54:10 +0200 |
| commit | cc69a4697633e14fc00c9bd0858b38120645464b (patch) | |
| tree | 6a589f6916cf85bbc008ef3db788db8b90056278 /kernel/mod_typing.mli | |
| parent | ff4d0d98ab0e0e81bd1acf9a7bf4b64913834911 (diff) | |
Univs: module constraints move to universe contexts as they might
declare new universes (e.g. with).
Diffstat (limited to 'kernel/mod_typing.mli')
| -rw-r--r-- | kernel/mod_typing.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli index b39e82125..80db12b0d 100644 --- a/kernel/mod_typing.mli +++ b/kernel/mod_typing.mli @@ -30,7 +30,7 @@ val translate_modtype : *) type 'alg translation = - module_signature * 'alg option * delta_resolver * Univ.constraints + module_signature * 'alg option * delta_resolver * Univ.ContextSet.t val translate_mse : env -> module_path option -> inline -> module_struct_entry -> |