diff options
| author | Matthieu Sozeau | 2017-07-20 15:45:17 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2018-07-25 17:56:21 +0200 |
| commit | cba9f3fe48817e8e524483fd984ea4938b3dc14f (patch) | |
| tree | 5ccc7b8297975c777e48d69c9918b0cb91fb9d19 /engine | |
| parent | 9b6ce4f1848c546d0d361aa1089fa2907ca4c9ad (diff) | |
kernel: missing check that all universes are declared.
Keep the universe_levels_of_constr function inside typeops, not
exported.
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/uState.ml | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/engine/uState.ml b/engine/uState.ml index 0791e4c277..b1fe91a21b 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -433,7 +433,7 @@ let univ_flexible_alg = UnivFlexible true let merge ?loc sideff rigid uctx ctx' = let open Univ in let levels = ContextSet.levels ctx' in - let uctx = if sideff then uctx else + let uctx = match rigid with | UnivRigid -> uctx | UnivFlexible b -> @@ -447,10 +447,7 @@ let merge ?loc sideff rigid uctx ctx' = uctx_univ_algebraic = LSet.union uctx.uctx_univ_algebraic levels } else { uctx with uctx_univ_variables = uvars' } in - let uctx_local = - if sideff then uctx.uctx_local - else ContextSet.append ctx' uctx.uctx_local - in + let uctx_local = ContextSet.append ctx' uctx.uctx_local in let declare g = LSet.fold (fun u g -> try UGraph.add_universe u false g |