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


From 6d998b5a0e6090b5c7d87d575016adc127b666d9 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 25 Jul 2018 18:34:06 +0200
Subject: Fix #7900 previous commit fixes a bug when using side effects in
 obligations.

Internal lemmas are inlined in obligations bodies, hence their universes
have to be declared with the obligations themselves. ~sideff:true was
not including the side effects universes and constraints in that case.
---
 engine/evd.ml     |  2 +-
 engine/uState.ml  | 17 +++++++++++++----
 engine/uState.mli |  2 +-
 3 files changed, 15 insertions(+), 6 deletions(-)

(limited to 'engine')

diff --git a/engine/evd.ml b/engine/evd.ml
index d1c7fef738..9f976b57dd 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -774,7 +774,7 @@ let universe_subst evd =
   UState.subst evd.universes
 
 let merge_context_set ?loc ?(sideff=false) rigid evd ctx' =
-  {evd with universes = UState.merge ?loc sideff rigid evd.universes ctx'}
+  {evd with universes = UState.merge ?loc ~sideff ~extend:true rigid evd.universes ctx'}
 
 let merge_universe_subst evd subst = 
   {evd with universes = UState.merge_subst evd.universes subst }
diff --git a/engine/uState.ml b/engine/uState.ml
index b1fe91a21b..29cb3c9bcc 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -430,10 +430,17 @@ let univ_rigid = UnivRigid
 let univ_flexible = UnivFlexible false
 let univ_flexible_alg = UnivFlexible true
 
-let merge ?loc sideff rigid uctx ctx' =
+(** ~sideff indicates that it is ok to redeclare a universe.
+    ~extend also merges the universe context in the local constraint structures
+    and not only in the graph. This depends if the
+    context we merge comes from a side effect that is already inlined
+    or defined separately. In the later case, there is no extension,
+    see [emit_side_effects] for example. *)
+let merge ?loc ~sideff ~extend rigid uctx ctx' =
   let open Univ in
   let levels = ContextSet.levels ctx' in
   let uctx =
+    if not extend then uctx else
     match rigid with
     | UnivRigid -> uctx
     | UnivFlexible b ->
@@ -447,7 +454,9 @@ 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 = ContextSet.append ctx' uctx.uctx_local in
+  let uctx_local =
+    if not extend then uctx.uctx_local
+    else ContextSet.append ctx' uctx.uctx_local in
   let declare g =
     LSet.fold (fun u g ->
                try UGraph.add_universe u false g
@@ -476,7 +485,7 @@ let merge_subst uctx s =
 
 let emit_side_effects eff u =
   let uctxs = Safe_typing.universes_of_private eff in
-  List.fold_left (merge true univ_rigid) u uctxs
+  List.fold_left (merge ~sideff:true ~extend:false univ_rigid) u uctxs
 
 let new_univ_variable ?loc rigid name
   ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) =
@@ -665,7 +674,7 @@ let update_sigma_env uctx env =
     { uctx with uctx_initial_universes = univs;
                          uctx_universes = univs }
   in
-  merge true univ_rigid eunivs eunivs.uctx_local
+  merge ~sideff:true ~extend:false univ_rigid eunivs eunivs.uctx_local
 
 let pr_weak prl {uctx_weak_constraints=weak} =
   let open Pp in
diff --git a/engine/uState.mli b/engine/uState.mli
index a59e61b894..f833508ebf 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -103,7 +103,7 @@ val univ_rigid : rigid
 val univ_flexible : rigid
 val univ_flexible_alg : rigid
 
-val merge : ?loc:Loc.t -> bool -> rigid -> t -> Univ.ContextSet.t -> t
+val merge : ?loc:Loc.t -> sideff:bool -> extend:bool -> rigid -> t -> Univ.ContextSet.t -> t
 val merge_subst : t -> UnivSubst.universe_opt_subst -> t
 val emit_side_effects : Safe_typing.private_constants -> t -> t
 
-- 
cgit v1.2.3