From cba9f3fe48817e8e524483fd984ea4938b3dc14f Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Thu, 20 Jul 2017 15:45:17 +0200
Subject: kernel: missing check that all universes are declared.

Keep the universe_levels_of_constr function inside typeops, not
exported.
---
 engine/uState.ml | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

(limited to 'engine')

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
-- 
cgit v1.2.3