Specialize UState.merge for extend:false

It's only called with extend:false from inside UState so we don't need
to expose it.

Not having to look at the whole `merge` function will hopefully help
those trying to understand side effects.

4 files changed, 37 insertions, 26 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 6a721a1a8a..e755af56c9 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -864,7 +864,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 ~extend:true rigid evd.universes ctx'}
+  {evd with universes = UState.merge ?loc ~sideff 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 6c1e70f54f..af714f6282 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -477,10 +477,9 @@ let univ_flexible_alg = UnivFlexible true
     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 merge ?loc ~sideff rigid uctx ctx' =
   let levels = ContextSet.levels ctx' in
   let uctx =
-    if not extend then uctx else
     match rigid with
     | UnivRigid -> uctx
     | UnivFlexible b ->
@@ -489,25 +488,23 @@ let merge ?loc ~sideff ~extend rigid uctx ctx' =
         else LMap.add u None accu
       in
       let uvars' = LSet.fold fold levels uctx.uctx_univ_variables in
-        if b then
-          { uctx with uctx_univ_variables = uvars';
-          uctx_univ_algebraic = LSet.union uctx.uctx_univ_algebraic levels }
-        else { uctx with uctx_univ_variables = uvars' }
+      if b then
+        { uctx with uctx_univ_variables = uvars';
+                    uctx_univ_algebraic = LSet.union uctx.uctx_univ_algebraic levels }
+      else { uctx with uctx_univ_variables = uvars' }
   in
-  let uctx_local =
-    if not extend 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 ~lbound:uctx.uctx_universes_lbound ~strict:false u g
-               with UGraph.AlreadyDeclared when sideff -> g)
-              levels g
+        try UGraph.add_universe ~lbound:uctx.uctx_universes_lbound ~strict:false u g
+        with UGraph.AlreadyDeclared when sideff -> g)
+      levels g
   in
   let uctx_names =
     let fold u accu =
       let modify _ info = match info.uloc with
-      | None -> { info with uloc = loc }
-      | Some _ -> info
+        | None -> { info with uloc = loc }
+        | Some _ -> info
       in
       try LMap.modify u modify accu
       with Not_found -> LMap.add u { uname = None; uloc = loc } accu
@@ -527,13 +524,35 @@ let demote_seff_univs (univs,_) uctx =
   let seff = LSet.union uctx.uctx_seff_univs univs in
   { uctx with uctx_seff_univs = seff }
 
+let merge_seff uctx ctx' =
+  let levels = ContextSet.levels ctx' in
+  let declare g =
+    LSet.fold (fun u g ->
+        try UGraph.add_universe ~lbound:uctx.uctx_universes_lbound ~strict:false u g
+        with UGraph.AlreadyDeclared -> g)
+      levels g
+  in
+  let initial = declare uctx.uctx_initial_universes in
+  let univs = declare uctx.uctx_universes in
+  let uctx_universes = UGraph.merge_constraints (ContextSet.constraints ctx') univs in
+  { uctx with uctx_universes;
+              uctx_initial_universes = initial }
+
 let emit_side_effects eff u =
   let uctxs = Safe_typing.universes_of_private eff in
   List.fold_left (fun u uctx ->
       let u = demote_seff_univs uctx u in
-      merge ~sideff:true ~extend:false univ_rigid u uctx)
+      merge_seff u uctx)
     u uctxs
 
+let update_sigma_env uctx env =
+  let univs = UGraph.make_sprop_cumulative (Environ.universes env) in
+  let eunivs =
+    { uctx with uctx_initial_universes = univs;
+                uctx_universes = univs }
+  in
+  merge_seff eunivs eunivs.uctx_local
+
 let new_univ_variable ?loc rigid name
   ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) =
   let u = UnivGen.fresh_level () in
@@ -729,14 +748,6 @@ let minimize uctx =
 let universe_of_name uctx s = 
   UNameMap.find s (fst uctx.uctx_names)
 
-let update_sigma_env uctx env =
-  let univs = UGraph.make_sprop_cumulative (Environ.universes env) in
-  let eunivs =
-    { uctx with uctx_initial_universes = univs;
-                         uctx_universes = univs }
-  in
-  merge ~sideff:true ~extend:false univ_rigid eunivs eunivs.uctx_local
-
 let pr_weak prl {uctx_weak_constraints=weak} =
   let open Pp in
   prlist_with_sep fnl (fun (u,v) -> prl u ++ str " ~ " ++ prl v) (UPairSet.elements weak)
diff --git a/engine/uState.mli b/engine/uState.mli
index 56a205c1e3..7cb2f49780 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -108,7 +108,7 @@ val univ_rigid : rigid
 val univ_flexible : rigid
 val univ_flexible_alg : rigid
 
-val merge : ?loc:Loc.t -> sideff:bool -> extend:bool -> rigid -> t -> Univ.ContextSet.t -> t
+val merge : ?loc:Loc.t -> sideff: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
 
diff --git a/tactics/pfedit.ml b/tactics/pfedit.ml
index f7634ba745..413c6540a3 100644
--- a/tactics/pfedit.ml
+++ b/tactics/pfedit.ml
@@ -140,7 +140,7 @@ let build_by_tactic ?(side_eff=true) env sigma ~poly typ tac =
     if side_eff then Safe_typing.inline_private_constants env (body, eff.Evd.seff_private)
     else body
   in
-  let univs = UState.merge ~sideff:side_eff ~extend:true Evd.univ_rigid univs ctx in
+  let univs = UState.merge ~sideff:side_eff Evd.univ_rigid univs ctx in
   cb, status, univs
 
 let refine_by_tactic ~name ~poly env sigma ty tac =