diff options
| author | Matthieu Sozeau | 2016-10-20 17:45:17 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-10-20 17:45:17 +0200 |
| commit | 3e536acf2ebcd078314dcac2a79d267c95db7bf8 (patch) | |
| tree | 39372d99951e30f1429b1d45a0a0844d9db8b588 /library | |
| parent | df1de9fa318f1924d92fb39c4bc67c16f3d31db4 (diff) | |
| parent | 474a58b15ca41f1b3287ef3e29e80cca9988598c (diff) | |
Merge branch 'bug5036' into v8.6
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/library/declare.ml b/library/declare.ml index c5b83c11a0..c9992fff3b 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -491,8 +491,10 @@ let do_universe poly l = type constraint_decl = polymorphic * Univ.constraints let cache_constraints (na, (p, c)) = - let ctx = Univ.ContextSet.add_constraints c Univ.ContextSet.empty in - cache_universe_context (p,ctx) + let ctx = + Univ.ContextSet.add_constraints c + Univ.ContextSet.empty (* No declared universes here, just constraints *) + in cache_universe_context (p,ctx) let discharge_constraints (_, (p, c as a)) = if p then None else Some a |