From ba86025e97d3ee110978592239131865f4187b1c Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 9 Oct 2019 15:00:55 +0200
Subject: Simplify universe handling wrt side effects: rm demote_seff_univs

We don't need to call `UState.demote_seff_univs` as
`emit_side_effects` (`tclEFFECTS`) can do it for us.
---
 engine/uState.ml  | 17 ++++++++---------
 engine/uState.mli |  2 --
 2 files changed, 8 insertions(+), 11 deletions(-)

(limited to 'engine')

diff --git a/engine/uState.ml b/engine/uState.ml
index d93ccafcf0..6c1e70f54f 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -463,14 +463,6 @@ let restrict ctx vars =
   let uctx' = restrict_universe_context ~lbound:ctx.uctx_universes_lbound ctx.uctx_local vars in
   { ctx with uctx_local = uctx' }
 
-let demote_seff_univs universes uctx =
-  let open Entries in
-  match universes with
-  | Polymorphic_entry _ -> uctx
-  | Monomorphic_entry (univs, _) ->
-    let seff = LSet.union uctx.uctx_seff_univs univs in
-    { uctx with uctx_seff_univs = seff }
-
 type rigid = 
   | UnivRigid
   | UnivFlexible of bool (** Is substitution by an algebraic ok? *)
@@ -531,9 +523,16 @@ let merge ?loc ~sideff ~extend rigid uctx ctx' =
 let merge_subst uctx s =
   { uctx with uctx_univ_variables = LMap.subst_union uctx.uctx_univ_variables s }
 
+let demote_seff_univs (univs,_) uctx =
+  let seff = LSet.union uctx.uctx_seff_univs univs in
+  { uctx with uctx_seff_univs = seff }
+
 let emit_side_effects eff u =
   let uctxs = Safe_typing.universes_of_private eff in
-  List.fold_left (merge ~sideff:true ~extend:false univ_rigid) u uctxs
+  List.fold_left (fun u uctx ->
+      let u = demote_seff_univs uctx u in
+      merge ~sideff:true ~extend:false univ_rigid u uctx)
+    u uctxs
 
 let new_univ_variable ?loc rigid name
   ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) =
diff --git a/engine/uState.mli b/engine/uState.mli
index 52e48c4eeb..56a205c1e3 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -100,8 +100,6 @@ val restrict_universe_context : lbound:Univ.Level.t -> ContextSet.t -> LSet.t ->
    universes are preserved. *)
 val restrict : t -> Univ.LSet.t -> t
 
-val demote_seff_univs : Entries.universes_entry -> t -> t
-
 type rigid = 
   | UnivRigid
   | UnivFlexible of bool (** Is substitution by an algebraic ok? *)
-- 
cgit v1.2.3