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.

3 files changed, 9 insertions, 13 deletions

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? *)
diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml
index 5be7b4fa28..f7634ba745 100644
--- a/tactics/pfedit.ml
+++ b/tactics/pfedit.ml
@@ -124,8 +124,7 @@ let build_constant_by_tactic ~name ctx sign ~poly typ tac =
     let { entries; universes } = close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x) pf in
     match entries with
     | [entry] ->
-      let univs = UState.demote_seff_univs entry.Declare.proof_entry_universes universes in
-      entry, status, univs
+      entry, status, universes
     | _ ->
       CErrors.anomaly Pp.(str "[build_constant_by_tactic] close_proof returned more than one proof term")
   with reraise ->