diff options
| author | Pierre-Marie Pédrot | 2015-10-02 16:27:58 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-10-02 16:33:15 +0200 |
| commit | 944c8de0bfe4048e0733a487e6388db4dfc9075a (patch) | |
| tree | af037ad2d990da53529356fec44860ad9ca87577 /kernel/declarations.mli | |
| parent | 16c88c9be5c37ee2e4fe04f7342365964031e7dd (diff) | |
| parent | 8860362de4a26286b0cb20cf4e02edc5209bdbd1 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'kernel/declarations.mli')
| -rw-r--r-- | kernel/declarations.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 561c66b422..7def963e73 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -246,8 +246,8 @@ and module_body = mod_type : module_signature; (** expanded type *) (** algebraic type, kept if it's relevant for extraction *) mod_type_alg : module_expression option; - (** set of all constraints in the module *) - mod_constraints : Univ.constraints; + (** set of all universes constraints in the module *) + mod_constraints : Univ.ContextSet.t; (** quotiented set of equivalent constants and inductive names *) mod_delta : Mod_subst.delta_resolver; mod_retroknowledge : Retroknowledge.action list } |